Search results for "CADE"

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

Publications at "CADE"( http://dblp.L3S.de/Venues/CADE )