


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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














