Automated deduction

InhaltsverzeichnisWhat 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.