default search action
20th CADE 2005: Tallinn, Estonia
- Robert Nieuwenhuis:
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings. Lecture Notes in Computer Science 3632, Springer 2005, ISBN 3-540-28005-7 - Gilles Dowek:
What Do We Know When We Know That a Theory Is Consistent?. 1-6 - Evelyne Contejean, Pierre Corbineau:
Reflecting Proofs in First-Order Logic with Equality. 7-22 - Chad E. Brown:
Reasoning in Extensional Type Theory with Equality. 23-37 - Christian Urban, Christine Tasson:
Nominal Techniques in Isabelle/HOL. 38-53 - Brigitte Pientka:
Tabling for Higher-Order Logic Programming. 54-68 - Kaustuv Chaudhuri, Frank Pfenning:
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. 69-83 - Serge Autexier:
The CoRe Calculus. 84-98 - Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh:
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. 99-115 - Guillaume Dufay, Amy P. Felty, Stan Matwin:
Privacy-Sensitive Information Flow with JML. 116-130 - Ting Zhang, Henny B. Sipma, Zohar Manna:
The Decidability of the First-Order Theory of Knuth-Bendix Order. 131-148 - Jordi Levy, Joachim Niehren, Mateu Villaret:
Well-Nested Context Unification. 149-163 - Guillem Godoy, Ashish Tiwari:
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules. 164-176 - Sean Bechhofer, Ian Horrocks, Daniele Turi:
The OWL Instance Store: System Description. 177-181 - Boris Konev, Frank Wolter, Michael Zakharyaschev:
Temporal Logics over Transitive States. 182-203 - Ullrich Hustadt, Boris Konev, Renate A. Schmidt:
Deciding Monodic Fragments by Temporal Resolution. 204-218 - Viorica Sofronie-Stokkermans:
Hierarchic Reasoning in Local Theory Extensions. 219-234 - Claudio Castellini, Alan Smaill:
Proof Planning for First-Order Temporal Logic. 235-249 - Andreas Meier, Erica Melis:
System Description: Multi A Multi-strategy Proof Planner. 250-254 - Randal E. Bryant, Sanjit A. Seshia:
Decision Procedures Customized for Formal Verification. 255-259 - Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard:
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. 260-277 - Franz Baader, Silvio Ghilardi:
Connecting Many-Sorted Theories. 278-294 - Sean McLaughlin, John Harrison:
A Proof-Producing Decision Procedure for Real Arithmetic. 295-314 - Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
The MathSAT 3 System. 315-321 - Graham Steel:
Deduction with XOR Constraints in Security API Modelling. 322-336 - Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick:
On the Complexity of Equational Horn Clauses. 337-352 - Greta Yorsh, Madanlal Musuvathi:
A Combination Method for Generating Interpolants. 353-368 - Marco Benedetti:
sKizzo: A Suite to Evaluate and Certify QBFs. 369-376 - Tomasz Truderung:
Regular Protocols and Attacks with Regular Knowledge. 377-391 - Peter Baumgartner, Cesare Tinelli:
The Model Evolution Calculus with Equality. 392-408 - Christian G. Fermüller, Reinhard Pichler:
Model Representation via Contexts and Implicit Generalizations. 409-423 - Mizuhito Ogawa, Eiichi Horita, Satoshi Ono:
Proving Properties of Incremental Merkle Trees. 424-440 - Jian Zhang:
Computer Search for Counterexamples to Wilkie's Identity. 441-451 - Alex Sinner, Thomas Kleemann:
KRHyper - In Your Pocket. 452-457
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.