Coverart for item
The Resource Automated deduction, CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings, Robert Nieuwenhuis (ed.)

Automated deduction, CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings, Robert Nieuwenhuis (ed.)

Label
Automated deduction, CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings
Title
Automated deduction, CADE-20
Title remainder
20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings
Statement of responsibility
Robert Nieuwenhuis (ed.)
Title variation
  • CADE-20
  • CADE-twenty
  • 20th International Conference on Automated Deduction
  • Twentieth International Conference on Automated Deduction
  • International Conference on Automated Deduction
  • CADE 2005
Creator
Contributor
Subject
Genre
Language
eng
Summary
"This volume contains the proceedings of the 20th International Conference on Automated Deduction (CADE-20). It was held July 22-27, 2005 in Tallinn, Estonia ..."
Member of
Cataloging source
GW5XE
Dewey number
006.3
Illustrations
illustrations
Index
index present
LC call number
QA76.9.A96
LC item number
I57 2005eb
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2005
http://bibfra.me/vocab/lite/meetingName
International Conference on Automated Deduction
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorName
Nieuwenhuis, Robert
Series statement
  • Lecture notes in computer science,
  • Lecture notes in artificial intelligence
Series volume
3632.
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • Logic, Symbolic and mathematical
  • COMPUTERS
  • COMPUTERS
  • Informatique
  • Automatic theorem proving
  • Logic, Symbolic and mathematical
  • Automatisches Beweisverfahren
  • Système déductif
  • Démonstration automatique de théorèmes
  • Reval <2005>
Label
Automated deduction, CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings, Robert Nieuwenhuis (ed.)
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
What Do We Know When We Know That a Theory Is Consistent? -- Reflecting Proofs in First-Order Logic with Equality -- Reasoning in Extensional Type Theory with Equality -- Nominal Techniques in Isabelle/HOL -- Tabling for Higher-Order Logic Programming -- A Focusing Inverse Method Theorem Prover for First-Order Linear Logic -- The CoRe Calculus -- Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures -- Privacy-Sensitive Information Flow with JML -- The Decidability of the First-Order Theory of Knuth-Bendix Order -- Well-Nested Context Unification -- Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules -- The OWL Instance Store: System Description -- Temporal Logics over Transitive States -- Deciding Monodic Fragments by Temporal Resolution -- Hierarchic Reasoning in Local Theory Extensions -- Proof Planning for First-Order Temporal Logic -- System Description: Multi A Multi-strategy Proof Planner -- Decision Procedures Customized for Formal Verification -- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic -- Connecting Many-Sorted Theories -- A Proof-Producing Decision Procedure for Real Arithmetic -- The MathSAT 3 System -- Deduction with XOR Constraints in Security API Modelling -- On the Complexity of Equational Horn Clauses -- A Combination Method for Generating Interpolants -- sKizzo: A Suite to Evaluate and Certify QBFs -- Regular Protocols and Attacks with Regular Knowledge -- The Model Evolution Calculus with Equality -- Model Representation via Contexts and Implicit Generalizations -- Proving Properties of Incremental Merkle Trees -- Computer Search for Counterexamples to Wilkie's Identity -- KRHyper -- In Your Pocket
Control code
262681806
Dimensions
unknown
Extent
1 online resource (xiii, 457 pages)
Form of item
online
Isbn
9783540280057
Lccn
2005929197
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/11532231
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-28005-7
Specific material designation
remote
System control number
(OCoLC)262681806
Label
Automated deduction, CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings, Robert Nieuwenhuis (ed.)
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
What Do We Know When We Know That a Theory Is Consistent? -- Reflecting Proofs in First-Order Logic with Equality -- Reasoning in Extensional Type Theory with Equality -- Nominal Techniques in Isabelle/HOL -- Tabling for Higher-Order Logic Programming -- A Focusing Inverse Method Theorem Prover for First-Order Linear Logic -- The CoRe Calculus -- Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures -- Privacy-Sensitive Information Flow with JML -- The Decidability of the First-Order Theory of Knuth-Bendix Order -- Well-Nested Context Unification -- Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules -- The OWL Instance Store: System Description -- Temporal Logics over Transitive States -- Deciding Monodic Fragments by Temporal Resolution -- Hierarchic Reasoning in Local Theory Extensions -- Proof Planning for First-Order Temporal Logic -- System Description: Multi A Multi-strategy Proof Planner -- Decision Procedures Customized for Formal Verification -- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic -- Connecting Many-Sorted Theories -- A Proof-Producing Decision Procedure for Real Arithmetic -- The MathSAT 3 System -- Deduction with XOR Constraints in Security API Modelling -- On the Complexity of Equational Horn Clauses -- A Combination Method for Generating Interpolants -- sKizzo: A Suite to Evaluate and Certify QBFs -- Regular Protocols and Attacks with Regular Knowledge -- The Model Evolution Calculus with Equality -- Model Representation via Contexts and Implicit Generalizations -- Proving Properties of Incremental Merkle Trees -- Computer Search for Counterexamples to Wilkie's Identity -- KRHyper -- In Your Pocket
Control code
262681806
Dimensions
unknown
Extent
1 online resource (xiii, 457 pages)
Form of item
online
Isbn
9783540280057
Lccn
2005929197
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/11532231
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-28005-7
Specific material designation
remote
System control number
(OCoLC)262681806

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125
Processing Feedback ...