Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Viktor Kuncak, Martin C. Rinard |
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Oleg Mürk, Daniel Larsson, Reiner Hähnle |
KeY-C: A Tool for Verification of C Programs. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Ulrich Furbach, Björn Pelzer |
Hyper Tableaux with Equality. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
Proving Termination by Bounded Increase. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Christian Urban, Stefan Berghofer, Michael Norrish |
Barendregt's Variable Convention in Rule Inductions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001 |
Logical Engineering with Instance-Based Methods. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Krauss 0001 |
Certified Size-Change Termination. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Osman Hasan, Sofiène Tahar |
Formalization of Continuous Probability Distributions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Juan Antonio Navarro Pérez, Andrei Voronkov |
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Colin Stirling |
Games, Automata and Matching. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Frank Pfenning (eds.) |
Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Gulay Ünel, David Toman 0001 |
An Incremental Technique for Automata-Based Decision Procedures. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Boris Motik, Robert D. C. Shearer, Ian Horrocks 0001 |
Optimized Reasoning in Description Logics Using Hypertableaux. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe, Yury Puzis |
SRASS - A Semantic Relevance Axiom Selection System. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Maria Paola Bonacina, Mnacho Echenim |
T-Decision by Decomposition. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | David Baelde, Andrew Gacek, Dale Miller 0001, Gopalan Nadathur, Alwen Tiu |
The Bedwyr System for Model Checking over Syntactic Expressions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Samuli Heilala, Brigitte Pientka |
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Mendonça de Moura, Nikolaj S. Bjørner |
Efficient E-Matching for SMT Solvers. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Guodong Li, Konrad Slind |
Compilation as Rewriting in Higher Order Logic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Falke 0001, Deepak Kapur |
Dependency Pairs for Rewriting with Non-free Constructors. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic |
System Description: SpassVersion 3.0. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Ashish Tiwari 0001, Sumit Gulwani |
Logical Interpretation: Static Program Analysis Using Theorem Proving. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin 0005, Christopher Lynch, Ralph Eric McGregor |
Encoding First Order Proofs in SAT. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Yeting Ge, Clark W. Barrett, Cesare Tinelli |
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Jean-François Couchot, Stéphane Lescuyer |
Handling Polymorphism in Automated Deduction. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Adam Koprowski, Aart Middeldorp |
Predictive Labeling with Dependency Pairs Using SAT. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Markus Aderhold |
Improvements in Formula Generalization. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
Labelled Clauses. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Christopher Lynch, Duc-Khanh Tran |
Automatic Decidability and Combinability Revisited. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Lutz, Frank Wolter |
Conservative Extensions in the Lightweight Description Logic EL. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | K. Rustan M. Leino |
Designing Verification Conditions for Software. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich |
System for Automated Deduction (SAD): A Tool for Proof Verification. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Claudio Castellini, Alan Smaill |
Proof Planning for First-Order Temporal Logic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Alex Sinner, Thomas Kleemann |
KRHyper - In Your Pocket. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Guillaume Dufay, Amy P. Felty, Stan Matwin |
Privacy-Sensitive Information Flow with JML. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis (eds.) |
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Marco Benedetti |
sKizzo: A Suite to Evaluate and Certify QBFs. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader, Silvio Ghilardi |
Connecting Many-Sorted Theories. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick |
On the Complexity of Equational Horn Clauses. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Cesare Tinelli |
The Model Evolution Calculus with Equality. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Sean Bechhofer, Ian Horrocks 0001, Daniele Turi |
The OWL Instance Store: System Description. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Jordi Levy, Joachim Niehren, Mateu Villaret |
Well-Nested Context Unification. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Christian Urban, Christine Tasson |
Nominal Techniques in Isabelle/HOL. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
theorem-assistants, Lambda-calculus, nominal logic, structural induction |
1 | Evelyne Contejean, Pierre Corbineau |
Reflecting Proofs in First-Order Logic with Equality. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Graham Steel |
Deduction with XOR Constraints in Security API Modelling. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Sean McLaughlin, John Harrison 0001 |
A Proof-Producing Decision Procedure for Real Arithmetic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Mizuhito Ogawa, Eiichi Horita, Satoshi Ono |
Proving Properties of Incremental Merkle Trees. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
temporal authentication, theorem prover, Merkle tree |
1 | Chad E. Brown |
Reasoning in Extensional Type Theory with Equality. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Ullrich Hustadt, Boris Konev, Renate A. Schmidt |
Deciding Monodic Fragments by Temporal Resolution. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Serge Autexier |
The CoRe Calculus. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Kaustuv Chaudhuri, Frank Pfenning |
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Tomasz Truderung |
Regular Protocols and Attacks with Regular Knowledge. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Viorica Sofronie-Stokkermans |
Hierarchic Reasoning in Local Theory Extensions. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Greta Yorsh, Madanlal Musuvathi |
A Combination Method for Generating Interpolants. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz 0001, Roberto Sebastiani |
The MathSAT 3 System. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava 0001, Greta Yorsh |
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Ting Zhang 0001, Henny B. Sipma, Zohar Manna |
The Decidability of the First-Order Theory of Knuth-Bendix Order. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Brigitte Pientka |
Tabling for Higher-Order Logic Programming. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Jian Zhang 0001 |
Computer Search for Counterexamples to Wilkie's Identity. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Guillem Godoy, Ashish Tiwari 0001 |
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Christian G. Fermüller, Reinhard Pichler |
Model Representation via Contexts and Implicit Generalizations. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
Model computation, clause evaluation, model representation |
1 | Andreas Meier 0002, Erica Melis |
System Description: Multi A Multi-strategy Proof Planner. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Boris Konev, Frank Wolter, Michael Zakharyaschev |
Temporal Logics over Transitive States. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek |
What Do We Know When We Know That a Theory Is Consistent?. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Randal E. Bryant, Sanjit A. Seshia |
Decision Procedures Customized for Formal Verification. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard |
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth |
How to Prove Inductive Theorems? QUODLIBET! |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Brigitte Pientka, Frank Pfenning |
Optimizing Higher-Order Pattern Unification. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner |
'Living Book': -'Deduction', 'Slicing', 'Interaction'. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Farhad Mehta, Tobias Nipkow |
Proving Pointer Programs in Higher-Order Logic. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Konstantin Korovin, Andrei Voronkov |
An AC-Compatible Knuth-Bendix Order. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Dimitri Hendriks, Vincent van Oostrom |
adbmal |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Giesl, Deepak Kapur |
Deciding Inductive Validity of Equations. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies |
The New WALDMEISTER Loop at Work. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Lutz, Ulrike Sattler, Lidia Tendera |
The Complexity of Finite Model Reasoning in Description Logics. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Johan G. F. Belinfante |
Reasoning about Iteration in Gödel's Class Theory. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch |
Unification Modulo ACU I Plus Homomorphisms/Distributivity. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
E-Unification, Rewrite reachability, Minskymachine, Complexity, Set constraints, Post correspondence problem |
1 | Panagiotis Manolios, Daron Vroon 0001 |
Algorithms for Ordinal Arithmetic. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Walther, Stephan Schweitzer |
About VeriFun. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Anthony G. Cohn 0001 |
Reasoning about Qualitative Representations of Space and Time. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | José Meseguer 0001, Miguel Palomino, Narciso Martí-Oliet |
Equational Abstractions. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Christopher Lynch |
Schematic Saturation for Decision and Unification Problems. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Manfred Schmidt-Schauß |
Decidability of Arity-Bounded Higher-Order Matching. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Jan Hladik, Ulrike Sattler |
A Translation of Looping Alternating Automata into Description Logics. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Cesare Tinelli |
The Model Evolution Calculus. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Ullrich Hustadt, Boris Konev |
TRP++2.0: A Temporal Resolution Prover. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Anatoli Degtyarev, Michael Fisher 0001, Boris Konev |
Monodic Temporal Resolution. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe, Christian B. Suttner |
The CADE-19 ATP System Competition. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002 |
Proof Search and Proof Check for Equational and Inductive Theorems. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant |
1 | Franz Baader (eds.) |
Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann |
Superposition Modulo a Shostak Theory. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Hans de Nivelle |
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Riazanov, Andrei Voronkov |
Efficient Instance Retrieval with Standard and Relational Path Indexing. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Karl Crary, Susmit Sarkar |
Foundational Certified Code in a Metalogical Framework. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Christophe Ringeissen |
Matching in a Class of Combined Non-disjoint Theories. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Lucas Dixon, Jacques D. Fleuriot |
IsaPlanner: A Prototype Proof Planner in Isabelle. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Greg Nelson |
Reasoning about Quantifiers by Matching in the E-graph. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Venkatesh Choppella, Christopher T. Haynes |
Source-Tracking Unification. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|