You have Guest access.
Log In
Robert Nieuwenhuis
Front matter
737
What Do We Know When We Know That a Theory Is Consistent?
736
Reflecting Proofs in First-Order Logic with Equality
738
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
736-737
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
737-738
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
739
Computer Search for Counterexamples to Wilkie’s Identity
KRHyper – In Your Pocket
Back matter
This page requires script.
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info