Search results for "CADE"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Simon Colton, Sophie Huczynska	The Homer System.	CADE	2003	DBLP DOI BibTeX RDF
1	Harald Ganzinger, Jürgen Stuber	Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation.	CADE	2003	DBLP DOI BibTeX RDF
1	Renate A. Schmidt, Ullrich Hustadt	A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.	CADE	2003	DBLP DOI BibTeX RDF
1	Nao Hirokawa, Aart Middeldorp	Automating the Dependency Pair Method.	CADE	2003	DBLP DOI BibTeX RDF
1	Aaron Stump	Subset Types and Partial Functions.	CADE	2003	DBLP DOI BibTeX RDF
1	Sava Krstic, Sylvain Conchon	Canonization for Disjoint Unions of Theories.	CADE	2003	DBLP DOI BibTeX RDF
1	Sumit Gulwani, George C. Necula	A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols.	CADE	2003	DBLP DOI BibTeX RDF
1	Guoqiang Pan, Moshe Y. Vardi	Optimizing a BDD-Based Modal Solver.	CADE	2003	DBLP DOI BibTeX RDF
1	Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge	Certifying Solutions to Permutation Group Problems.	CADE	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke	SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.	CADE	2003	DBLP DOI BibTeX RDF
1	Joe Hurd	An LCF-Style Interface between HOL and First-Order Logic.	CADE	2002	DBLP DOI BibTeX RDF
1	Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi	The Complexity of the Graded µ-Calculus.	CADE	2002	DBLP DOI BibTeX RDF
1	Dominique Larchey-Wendling	Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic.	CADE	2002	DBLP DOI BibTeX RDF
1	Jürgen Zimmer, Michael Kohlhase	System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning.	CADE	2002	DBLP DOI BibTeX RDF
1	Jonathan Ford, Natarajan Shankar	Formal Verification of a Combination Decision Procedure.	CADE	2002	DBLP DOI BibTeX RDF
1	Mateja Jamnik, Manfred Kerber, Martin Pollet	Learn Omega-matic: System Description.	CADE	2002	DBLP DOI BibTeX RDF
1	Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani	A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.	CADE	2002	DBLP DOI BibTeX RDF
1	Thierry Boy de la Tour	A Note on Symmetry Heuristics in SEM.	CADE	2002	DBLP DOI BibTeX RDF
1	Simon Colton	The HR Program for Theorem Generation.	CADE	2002	DBLP DOI BibTeX RDF
1	Martin Strecker	Formal Verification of a Java Compiler in Isabelle.	CADE	2002	DBLP DOI BibTeX RDF
1	Jörg H. Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke 0001, Helmut Horacek, Michael Kohlhase, Andreas Meier 0002, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer	Proof Development with OMEGA.	CADE	2002	DBLP DOI BibTeX RDF
1	Miquel Bofill, Albert Rubio	Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation.	CADE	2002	DBLP DOI BibTeX RDF
1	Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic	S PASS Version 2.0.	CADE	2002	DBLP DOI BibTeX RDF
1	Chad E. Brown	Solving for Set Variables in Higher-Order Theorem Proving.	CADE	2002	DBLP DOI BibTeX RDF
1	Michael W. Whalen, Johann Schumann, Bernd Fischer 0002	AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description.	CADE	2002	DBLP DOI BibTeX RDF
1	Jean-Marc Andreoli	Focussing Proof-Net Construction as a Middleware Paradigm.	CADE	2002	DBLP DOI BibTeX RDF	Proof construction, Focussing, Middleware, Transactions, Proof search, Proof-nets
1	Cristina Borralleras, Salvador Lucas, Albert Rubio	Recursive Path Orderings Can Be Context-Sensitive.	CADE	2002	DBLP DOI BibTeX RDF
1	Didier Galmiche, Daniel Méry	Connection-Based Proof Search in Propositional BI Logic.	CADE	2002	DBLP DOI BibTeX RDF
1	Uwe Egly	Embedding Lax Logic into Intuitionistic Logic.	CADE	2002	DBLP DOI BibTeX RDF
1	Calogero G. Zarba	Combining Multisets with Integers.	CADE	2002	DBLP DOI BibTeX RDF
1	Aaron Stump, David L. Dill	Faster Proof Checking in the Edinburgh Logical Framework.	CADE	2002	DBLP DOI BibTeX RDF
1	Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt	A New Clausal Class Decidable by Hyperresolution.	CADE	2002	DBLP DOI BibTeX RDF
1	Carlos Areces, Juan Heguiabehere	HyLoRes 1.0: Direct Resolution for Hybrid Logics.	CADE	2002	DBLP DOI BibTeX RDF
1	Bernhard Gramlich, Reinhard Pichler	Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations.	CADE	2002	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea	Lazy Theorem Proving for Bounded Model Checking over Infinite Domains.	CADE	2002	DBLP DOI BibTeX RDF
1	Harald Ganzinger	Shostak Light.	CADE	2002	DBLP DOI BibTeX RDF
1	Andrew Bernard, Peter Lee 0001	Temporal Logic for Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF	temporal logic, Proof-carrying code
1	Christopher Lynch, Barbara Morawska 0001	Basic Syntactic Mutation.	CADE	2002	DBLP DOI BibTeX RDF
1	Eugene Goldberg	Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points.	CADE	2002	DBLP DOI BibTeX RDF
1	Jesper B. Møller	DDDLIB: A Library for Solving Quantified Difference Inequalities.	CADE	2002	DBLP DOI BibTeX RDF
1	Andrei Voronkov (eds.)	Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings	CADE	2002	DBLP DOI BibTeX RDF
1	Lawrence C. Paulson	The Reflection Theorem: A Study in Meta-theoretic Reasoning.	CADE	2002	DBLP DOI BibTeX RDF
1	Stephan Schulz 0001, Geoff Sutcliffe	System Description: GrAnDe 1.0.	CADE	2002	DBLP DOI BibTeX RDF
1	Gilles Audemard, Belaid Benhamou	Reasoning by Symmetry and Function Ordering in Finite Model Generation.	CADE	2002	DBLP DOI BibTeX RDF
1	Matthias Baaz	Proof Analysis by Resolution.	CADE	2002	DBLP DOI BibTeX RDF
1	Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi	BDD-Based Decision Procedures for K.	CADE	2002	DBLP DOI BibTeX RDF
1	Thomas Hillenbrand, Bernd Löchner	The Next W ALDMEISTER Loop.	CADE	2002	DBLP DOI BibTeX RDF
1	Lintao Zhang, Sharad Malik	The Quest for Efficient Boolean Satisfiability Solvers.	CADE	2002	DBLP DOI BibTeX RDF
1	Ian Horrocks 0001	Reasoning with Expressive Description Logics: Theory and Practice.	CADE	2002	DBLP DOI BibTeX RDF
1	Robert R. Schneck, George C. Necula	A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF
1	Wolfgang Ahrendt	Deductive Search for Errors in Free Data Type Specifications Using Model Generation.	CADE	2002	DBLP DOI BibTeX RDF
1	Carsten Schürmann	Workshop: Automation of Proofs by Mathematical Induction.	CADE	2000	DBLP DOI BibTeX RDF
1	John Harrison 0001	High-Level Verification Using Theorem Proving and Formalized Mathematics.	CADE	2000	DBLP DOI BibTeX RDF
1	Marc Bezem, Dimitri Hendriks, Hans de Nivelle	Automated Proof Construction in Type Theory Using Resolution.	CADE	2000	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe	System Description: SystemOn TPTP.	CADE	2000	DBLP DOI BibTeX RDF
1	Carsten Schürmann	Tutorial: Meta-logical Frameworks.	CADE	2000	DBLP DOI BibTeX RDF
1	Stephen G. Pulman	Tutorial: Automated Deduction and Natural Language Understanding.	CADE	2000	DBLP DOI BibTeX RDF
1	Gilles Audemard, Belaid Benhamou, Laurent Henocque	Two Techniques to Improve Finite Model Search.	CADE	2000	DBLP DOI BibTeX RDF
1	Renate A. Schmidt, Ullrich Hustadt	A Resolution Decision Procedure for Fluted Logic.	CADE	2000	DBLP DOI BibTeX RDF
1	Erica Melis	Workshop: Automated Deduction in Education.	CADE	2000	DBLP DOI BibTeX RDF
1	Simon Colton, Volker Sorge, Ursula Martin	Workshop: The Role of Automated Deduction in Mathematics.	CADE	2000	DBLP DOI BibTeX RDF
1	Graham Collins, Louise A. Dennis	System Description: Embedding Verification into Microsoft Excel.	CADE	2000	DBLP DOI BibTeX RDF
1	Peter B. Andrews, Chad E. Brown	Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic.	CADE	2000	DBLP DOI BibTeX RDF
1	Doron Bustan, Orna Grumberg	Simulation Based Minimization.	CADE	2000	DBLP DOI BibTeX RDF
1	George C. Necula, Peter Lee 0001	Proof Generation in the Touchstone Theorem Prover.	CADE	2000	DBLP DOI BibTeX RDF
1	Mike Jackson 0003, Helen Lowe	System Description: Interactive Proof Critics in XBarnacle.	CADE	2000	DBLP DOI BibTeX RDF
1	Ian Horrocks 0001, Ulrike Sattler, Stephan Tobies	Reasoning with Individuals for the Description Logic SHIQ.	CADE	2000	DBLP DOI BibTeX RDF
1	Bruce Spencer, Joseph Douglas Horton	Support Ordered Resolution.	CADE	2000	DBLP DOI BibTeX RDF
1	Andreas Meier 0002	System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level.	CADE	2000	DBLP DOI BibTeX RDF
1	Carl-Johan H. Seger	Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice.	CADE	2000	DBLP DOI BibTeX RDF
1	Peter Baumgartner 0001	FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure.	CADE	2000	DBLP DOI BibTeX RDF
1	Neophytos G. Michael, Andrew W. Appel	Machine Instruction Syntax and Semantics in Higher Order Logic.	CADE	2000	DBLP DOI BibTeX RDF
1	Konrad Slind	Wellfounded Schematic Definitions.	CADE	2000	DBLP DOI BibTeX RDF
1	E. Allen Emerson, Vineet Kahlon	Reducing Model Checking of the Many to the Few.	CADE	2000	DBLP DOI BibTeX RDF
1	Clark W. Barrett, David L. Dill, Aaron Stump	A Framework for Cooperating Decision Procedures.	CADE	2000	DBLP DOI BibTeX RDF
1	Carsten Sinz	System Description: ARA - An Automatic Theorem Prover for Relation Algebras.	CADE	2000	DBLP DOI BibTeX RDF
1	Thomas Genet, Francis Klay	Rewriting for Cryptographic Protocol Verification.	CADE	2000	DBLP DOI BibTeX RDF
1	Peter B. Andrews, Matthew Bishop, Chad E. Brown	System Description: TPS: A Theorem Proving System for Type Theory.	CADE	2000	DBLP DOI BibTeX RDF
1	William M. Farmer	An Infrastructure for Intertheory Reasoning.	CADE	2000	DBLP DOI BibTeX RDF
1	Florian Kammüller	Modular Reasoning in Isabelle.	CADE	2000	DBLP DOI BibTeX RDF
1	Guillaume Gillard	A Formalization of a Concurrent Object Calculus up to alpha-Conversion.	CADE	2000	DBLP DOI BibTeX RDF
1	Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo	The Nuprl Open Logical Environment.	CADE	2000	DBLP DOI BibTeX RDF
1	Johan G. F. Belinfante	Gödel's Algorithm for Class Formation.	CADE	2000	DBLP DOI BibTeX RDF
1	Ashish Tiwari 0001, Leo Bachmair, Harald Rueß	Rigid E-Unification Revisited.	CADE	2000	DBLP DOI BibTeX RDF
1	Anatoli Degtyarev, Andrei Voronkov	Stratified Resolution.	CADE	2000	DBLP DOI BibTeX RDF
1	Leo Bachmair, Ashish Tiwari 0001	Abstract Congruence Closure and Specializations.	CADE	2000	DBLP DOI BibTeX RDF
1	David A. McAllester (eds.)	Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings	CADE	2000	DBLP DOI BibTeX RDF
1	Enrico Giunchiglia, Armando Tacchella	System Description: *SAT: A Platform for the Development of Modal Decision Procedures.	CADE	2000	DBLP DOI BibTeX RDF
1	Jürgen Giesl, Aart Middeldorp	Eliminating Dummy Elimination.	CADE	2000	DBLP DOI BibTeX RDF
1	Henry A. Kautz	Scalable Knowledge Representation and Reasoning Systems.	CADE	2000	DBLP DOI BibTeX RDF
1	Andreas Franke 0001, Michael Kohlhase	System Description: MBASE, an Open Mathematical Knowledge Base.	CADE	2000	DBLP DOI BibTeX RDF
1	Deepak Kapur, Mahadevan Subramaniam	Extending Decision Procedures with Induction Schemes.	CADE	2000	DBLP DOI BibTeX RDF
1	Cristina Borralleras, Maria Ferreira, Albert Rubio	Complete Monotonic Semantic Path Orderings.	CADE	2000	DBLP DOI BibTeX RDF
1	Ryuzo Hasegawa, Hiroshi Fujita 0002, Miyuki Koshimura	Efficient Minimal Model Generation Using Branching Lemmas.	CADE	2000	DBLP DOI BibTeX RDF
1	Peter Baumgartner 0001, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang 0001	Workshop: Model Computation - Principles, Algorithms, Applications.	CADE	2000	DBLP DOI BibTeX RDF
1	Peter F. Patel-Schneider	System Description: DLP.	CADE	2000	DBLP DOI BibTeX RDF
1	Didier Galmiche	Workshop: Type-Theoretic Languages: Proof-Search and Semantics.	CADE	2000	DBLP DOI BibTeX RDF
1	Viorica Sofronie-Stokkermans	On Unification for Bonded Distributive Lattices.	CADE	2000	DBLP DOI BibTeX RDF
1	Marianne Brown, Geoff Sutcliffe	System Description: PTTP+GLiDes: Semantically Guided PTTP.	CADE	2000	DBLP DOI BibTeX RDF
1	William McCune, Olga Shumsky	System Description: IVY.	CADE	2000	DBLP DOI BibTeX RDF

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