Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
27	Gilles Dowek	What Do We Know When We Know That a Theory Is Consistent?.	CADE	2005	DBLP DOI BibTeX RDF
27	Randal E. Bryant, Sanjit A. Seshia	Decision Procedures Customized for Formal Verification.	CADE	2005	DBLP DOI BibTeX RDF
27	Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard	An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic.	CADE	2005	DBLP DOI BibTeX RDF
27	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
27	Dieter Hutter	Deduction as an Engineering Science.	FTP	2003	DBLP DOI BibTeX RDF
27	Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth	How to Prove Inductive Theorems? QUODLIBET!	CADE	2003	DBLP DOI BibTeX RDF
27	Brigitte Pientka, Frank Pfenning	Optimizing Higher-Order Pattern Unification.	CADE	2003	DBLP DOI BibTeX RDF
27	Farhad Mehta, Tobias Nipkow	Proving Pointer Programs in Higher-Order Logic.	CADE	2003	DBLP DOI BibTeX RDF
27	Dimitri Hendriks, Vincent van Oostrom	adbmal	CADE	2003	DBLP DOI BibTeX RDF
27	Jürgen Giesl, Deepak Kapur	Deciding Inductive Validity of Equations.	CADE	2003	DBLP DOI BibTeX RDF
27	Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies	The New WALDMEISTER Loop at Work.	CADE	2003	DBLP DOI BibTeX RDF
27	Carsten Lutz, Ulrike Sattler, Lidia Tendera	The Complexity of Finite Model Reasoning in Description Logics.	CADE	2003	DBLP DOI BibTeX RDF
27	Johan G. F. Belinfante	Reasoning about Iteration in Gödel's Class Theory.	CADE	2003	DBLP DOI BibTeX RDF
27	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
27	Panagiotis Manolios, Daron Vroon 0001	Algorithms for Ordinal Arithmetic.	CADE	2003	DBLP DOI BibTeX RDF
27	Christoph Walther, Stephan Schweitzer	About VeriFun.	CADE	2003	DBLP DOI BibTeX RDF
27	Anthony G. Cohn 0001	Reasoning about Qualitative Representations of Space and Time.	CADE	2003	DBLP DOI BibTeX RDF
27	José Meseguer 0001, Miguel Palomino, Narciso Martí-Oliet	Equational Abstractions.	CADE	2003	DBLP DOI BibTeX RDF
27	Christopher Lynch	Schematic Saturation for Decision and Unification Problems.	CADE	2003	DBLP DOI BibTeX RDF
27	Manfred Schmidt-Schauß	Decidability of Arity-Bounded Higher-Order Matching.	CADE	2003	DBLP DOI BibTeX RDF
27	Jan Hladik, Ulrike Sattler	A Translation of Looping Alternating Automata into Description Logics.	CADE	2003	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Cesare Tinelli	The Model Evolution Calculus.	CADE	2003	DBLP DOI BibTeX RDF
27	Ullrich Hustadt, Boris Konev	TRP++2.0: A Temporal Resolution Prover.	CADE	2003	DBLP DOI BibTeX RDF
27	Anatoli Degtyarev, Michael Fisher 0001, Boris Konev	Monodic Temporal Resolution.	CADE	2003	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe, Christian B. Suttner	The CADE-19 ATP System Competition.	CADE	2003	DBLP DOI BibTeX RDF
27	Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann	Superposition Modulo a Shostak Theory.	CADE	2003	DBLP DOI BibTeX RDF
27	Alexandre Riazanov, Andrei Voronkov	Efficient Instance Retrieval with Standard and Relational Path Indexing.	CADE	2003	DBLP DOI BibTeX RDF
27	Karl Crary, Susmit Sarkar	Foundational Certified Code in a Metalogical Framework.	CADE	2003	DBLP DOI BibTeX RDF
27	Lucas Dixon, Jacques D. Fleuriot	IsaPlanner: A Prototype Proof Planner in Isabelle.	CADE	2003	DBLP DOI BibTeX RDF
27	Greg Nelson	Reasoning about Quantifiers by Matching in the E-graph.	CADE	2003	DBLP DOI BibTeX RDF
27	Venkatesh Choppella, Christopher T. Haynes	Source-Tracking Unification.	CADE	2003	DBLP DOI BibTeX RDF
27	Simon Colton, Sophie Huczynska	The Homer System.	CADE	2003	DBLP DOI BibTeX RDF
27	Harald Ganzinger, Jürgen Stuber	Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation.	CADE	2003	DBLP DOI BibTeX RDF
27	Renate A. Schmidt, Ullrich Hustadt	A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.	CADE	2003	DBLP DOI BibTeX RDF
27	Nao Hirokawa, Aart Middeldorp	Automating the Dependency Pair Method.	CADE	2003	DBLP DOI BibTeX RDF
27	Aaron Stump	Subset Types and Partial Functions.	CADE	2003	DBLP DOI BibTeX RDF
27	Sava Krstic, Sylvain Conchon	Canonization for Disjoint Unions of Theories.	CADE	2003	DBLP DOI BibTeX RDF
27	Sumit Gulwani, George C. Necula	A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols.	CADE	2003	DBLP DOI BibTeX RDF
27	Guoqiang Pan, Moshe Y. Vardi	Optimizing a BDD-Based Modal Solver.	CADE	2003	DBLP DOI BibTeX RDF
27	Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge	Certifying Solutions to Permutation Group Problems.	CADE	2003	DBLP DOI BibTeX RDF
27	Edmund M. Clarke	SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.	CADE	2003	DBLP DOI BibTeX RDF
27	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
27	Joe Hurd	An LCF-Style Interface between HOL and First-Order Logic.	CADE	2002	DBLP DOI BibTeX RDF
27	Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi	The Complexity of the Graded µ-Calculus.	CADE	2002	DBLP DOI BibTeX RDF
27	Dominique Larchey-Wendling	Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic.	CADE	2002	DBLP DOI BibTeX RDF
27	Jürgen Zimmer, Michael Kohlhase	System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning.	CADE	2002	DBLP DOI BibTeX RDF
27	Jonathan Ford, Natarajan Shankar	Formal Verification of a Combination Decision Procedure.	CADE	2002	DBLP DOI BibTeX RDF
27	Mateja Jamnik, Manfred Kerber, Martin Pollet	Learn Omega-matic: System Description.	CADE	2002	DBLP DOI BibTeX RDF
27	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
27	Thierry Boy de la Tour	A Note on Symmetry Heuristics in SEM.	CADE	2002	DBLP DOI BibTeX RDF
27	Simon Colton	The HR Program for Theorem Generation.	CADE	2002	DBLP DOI BibTeX RDF
27	Martin Strecker	Formal Verification of a Java Compiler in Isabelle.	CADE	2002	DBLP DOI BibTeX RDF
27	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
27	Miquel Bofill, Albert Rubio	Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation.	CADE	2002	DBLP DOI BibTeX RDF
27	Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic	S PASS Version 2.0.	CADE	2002	DBLP DOI BibTeX RDF
27	Chad E. Brown	Solving for Set Variables in Higher-Order Theorem Proving.	CADE	2002	DBLP DOI BibTeX RDF
27	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
27	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
27	Cristina Borralleras, Salvador Lucas, Albert Rubio	Recursive Path Orderings Can Be Context-Sensitive.	CADE	2002	DBLP DOI BibTeX RDF
27	Didier Galmiche, Daniel Méry	Connection-Based Proof Search in Propositional BI Logic.	CADE	2002	DBLP DOI BibTeX RDF
27	Uwe Egly	Embedding Lax Logic into Intuitionistic Logic.	CADE	2002	DBLP DOI BibTeX RDF
27	Calogero G. Zarba	Combining Multisets with Integers.	CADE	2002	DBLP DOI BibTeX RDF
27	Aaron Stump, David L. Dill	Faster Proof Checking in the Edinburgh Logical Framework.	CADE	2002	DBLP DOI BibTeX RDF
27	Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt	A New Clausal Class Decidable by Hyperresolution.	CADE	2002	DBLP DOI BibTeX RDF
27	Carlos Areces, Juan Heguiabehere	HyLoRes 1.0: Direct Resolution for Hybrid Logics.	CADE	2002	DBLP DOI BibTeX RDF
27	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
27	Harald Ganzinger	Shostak Light.	CADE	2002	DBLP DOI BibTeX RDF
27	Andrew Bernard, Peter Lee 0001	Temporal Logic for Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF	temporal logic, Proof-carrying code
27	Christopher Lynch, Barbara Morawska 0001	Basic Syntactic Mutation.	CADE	2002	DBLP DOI BibTeX RDF
27	Eugene Goldberg	Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points.	CADE	2002	DBLP DOI BibTeX RDF
27	Jesper B. Møller	DDDLIB: A Library for Solving Quantified Difference Inequalities.	CADE	2002	DBLP DOI BibTeX RDF
27	Lawrence C. Paulson	The Reflection Theorem: A Study in Meta-theoretic Reasoning.	CADE	2002	DBLP DOI BibTeX RDF
27	Stephan Schulz 0001, Geoff Sutcliffe	System Description: GrAnDe 1.0.	CADE	2002	DBLP DOI BibTeX RDF
27	Gilles Audemard, Belaid Benhamou	Reasoning by Symmetry and Function Ordering in Finite Model Generation.	CADE	2002	DBLP DOI BibTeX RDF
27	Matthias Baaz	Proof Analysis by Resolution.	CADE	2002	DBLP DOI BibTeX RDF
27	Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi	BDD-Based Decision Procedures for K.	CADE	2002	DBLP DOI BibTeX RDF
27	Thomas Hillenbrand, Bernd Löchner	The Next W ALDMEISTER Loop.	CADE	2002	DBLP DOI BibTeX RDF
27	Lintao Zhang, Sharad Malik	The Quest for Efficient Boolean Satisfiability Solvers.	CADE	2002	DBLP DOI BibTeX RDF
27	Ian Horrocks 0001	Reasoning with Expressive Description Logics: Theory and Practice.	CADE	2002	DBLP DOI BibTeX RDF
27	Robert R. Schneck, George C. Necula	A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF
27	Wolfgang Ahrendt	Deductive Search for Errors in Free Data Type Specifications Using Model Generation.	CADE	2002	DBLP DOI BibTeX RDF
27	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
27	Carsten Schürmann	Workshop: Automation of Proofs by Mathematical Induction.	CADE	2000	DBLP DOI BibTeX RDF
27	John Harrison 0001	High-Level Verification Using Theorem Proving and Formalized Mathematics.	CADE	2000	DBLP DOI BibTeX RDF
27	Marc Bezem, Dimitri Hendriks, Hans de Nivelle	Automated Proof Construction in Type Theory Using Resolution.	CADE	2000	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe	System Description: SystemOn TPTP.	CADE	2000	DBLP DOI BibTeX RDF
27	Gilles Audemard, Belaid Benhamou, Laurent Henocque	Two Techniques to Improve Finite Model Search.	CADE	2000	DBLP DOI BibTeX RDF
27	Renate A. Schmidt, Ullrich Hustadt	A Resolution Decision Procedure for Fluted Logic.	CADE	2000	DBLP DOI BibTeX RDF
27	Graham Collins, Louise A. Dennis	System Description: Embedding Verification into Microsoft Excel.	CADE	2000	DBLP DOI BibTeX RDF
27	Doron Bustan, Orna Grumberg	Simulation Based Minimization.	CADE	2000	DBLP DOI BibTeX RDF
27	George C. Necula, Peter Lee 0001	Proof Generation in the Touchstone Theorem Prover.	CADE	2000	DBLP DOI BibTeX RDF
27	Mike Jackson 0003, Helen Lowe	System Description: Interactive Proof Critics in XBarnacle.	CADE	2000	DBLP DOI BibTeX RDF
27	Ian Horrocks 0001, Ulrike Sattler, Stephan Tobies	Reasoning with Individuals for the Description Logic SHIQ.	CADE	2000	DBLP DOI BibTeX RDF
27	Bruce Spencer, Joseph Douglas Horton	Support Ordered Resolution.	CADE	2000	DBLP DOI BibTeX RDF
27	Carl-Johan H. Seger	Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice.	CADE	2000	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001	FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure.	CADE	2000	DBLP DOI BibTeX RDF
27	Neophytos G. Michael, Andrew W. Appel	Machine Instruction Syntax and Semantics in Higher Order Logic.	CADE	2000	DBLP DOI BibTeX RDF
27	Konrad Slind	Wellfounded Schematic Definitions.	CADE	2000	DBLP DOI BibTeX RDF
27	E. Allen Emerson, Vineet Kahlon	Reducing Model Checking of the Many to the Few.	CADE	2000	DBLP DOI BibTeX RDF
27	Clark W. Barrett, David L. Dill, Aaron Stump	A Framework for Cooperating Decision Procedures.	CADE	2000	DBLP DOI BibTeX RDF