04110nam 22006855 450 991048399080332120251226203404.010.1007/11532231(CKB)1000000000213153(SSID)ssj0000316395(PQKBManifestationID)11223740(PQKBTitleCode)TC0000316395(PQKBWorkID)10274877(PQKB)11751889(DE-He213)978-3-540-31864-4(MiAaPQ)EBC3067585(PPN)123096405(EXLCZ)99100000000021315320100721d2005 u| 0engurnn|008mamaatxtccrAutomated Deduction – CADE-20 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings /edited by Robert Nieuwenhuis1st ed. 2005.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2005.1 online resource (XIV, 466 p.) Lecture Notes in Artificial Intelligence,2945-9141 ;3632Bibliographic Level Mode of Issuance: Monograph3-540-31864-X 3-540-28005-7 Includes bibliographical references and index.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.Lecture Notes in Artificial Intelligence,2945-9141 ;3632Artificial intelligenceMachine theoryComputer scienceSoftware engineeringArtificial IntelligenceFormal Languages and Automata TheoryComputer Science Logic and Foundations of ProgrammingSoftware EngineeringArtificial intelligence.Machine theory.Computer science.Software engineering.Artificial Intelligence.Formal Languages and Automata Theory.Computer Science Logic and Foundations of Programming.Software Engineering.006.3Nieuwenhuis Robert1757739MiAaPQMiAaPQMiAaPQBOOK9910483990803321Automated Deduction – CADE-204522720UNINA