Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link
27	Carsten Sinz	System Description: ARA - An Automatic Theorem Prover for Relation Algebras.	CADE	2000	DBLP DOI BibTeX RDF
27	Thomas Genet, Francis Klay	Rewriting for Cryptographic Protocol Verification.	CADE	2000	DBLP DOI BibTeX RDF
27	Peter B. Andrews, Matthew Bishop, Chad E. Brown	System Description: TPS: A Theorem Proving System for Type Theory.	CADE	2000	DBLP DOI BibTeX RDF
27	William M. Farmer	An Infrastructure for Intertheory Reasoning.	CADE	2000	DBLP DOI BibTeX RDF
27	Florian Kammüller	Modular Reasoning in Isabelle.	CADE	2000	DBLP DOI BibTeX RDF
27	Guillaume Gillard	A Formalization of a Concurrent Object Calculus up to alpha-Conversion.	CADE	2000	DBLP DOI BibTeX RDF
27	Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo	The Nuprl Open Logical Environment.	CADE	2000	DBLP DOI BibTeX RDF
27	Johan G. F. Belinfante	Gödel's Algorithm for Class Formation.	CADE	2000	DBLP DOI BibTeX RDF
27	Ashish Tiwari 0001, Leo Bachmair, Harald Rueß	Rigid E-Unification Revisited.	CADE	2000	DBLP DOI BibTeX RDF
27	Anatoli Degtyarev, Andrei Voronkov	Stratified Resolution.	CADE	2000	DBLP DOI BibTeX RDF
27	Leo Bachmair, Ashish Tiwari 0001	Abstract Congruence Closure and Specializations.	CADE	2000	DBLP DOI BibTeX RDF
27	Jürgen Giesl, Aart Middeldorp	Eliminating Dummy Elimination.	CADE	2000	DBLP DOI BibTeX RDF
27	Henry A. Kautz	Scalable Knowledge Representation and Reasoning Systems.	CADE	2000	DBLP DOI BibTeX RDF
27	Andreas Franke 0001, Michael Kohlhase	System Description: MBASE, an Open Mathematical Knowledge Base.	CADE	2000	DBLP DOI BibTeX RDF
27	Deepak Kapur, Mahadevan Subramaniam	Extending Decision Procedures with Induction Schemes.	CADE	2000	DBLP DOI BibTeX RDF
27	Cristina Borralleras, Maria Ferreira, Albert Rubio	Complete Monotonic Semantic Path Orderings.	CADE	2000	DBLP DOI BibTeX RDF
27	Ryuzo Hasegawa, Hiroshi Fujita 0002, Miyuki Koshimura	Efficient Minimal Model Generation Using Branching Lemmas.	CADE	2000	DBLP DOI BibTeX RDF
27	Peter F. Patel-Schneider	System Description: DLP.	CADE	2000	DBLP DOI BibTeX RDF
27	Didier Galmiche	Workshop: Type-Theoretic Languages: Proof-Search and Semantics.	CADE	2000	DBLP DOI BibTeX RDF
27	Viorica Sofronie-Stokkermans	On Unification for Bonded Distributive Lattices.	CADE	2000	DBLP DOI BibTeX RDF
27	William McCune, Olga Shumsky	System Description: IVY.	CADE	2000	DBLP DOI BibTeX RDF
27	Philippe Chatalic, Laurent Simon	ZRES: The Old Davis-Putman Procedure Meets ZBDD.	CADE	2000	DBLP DOI BibTeX RDF
27	Harald Ganzinger (eds.)	Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings	CADE	1999	DBLP DOI BibTeX RDF
27	Olga Caprotti, Arjeh M. Cohen	Integrating computational and deduction systems using OpenMath.	Calculemus	1999	DBLP DOI BibTeX RDF
27	Jon Whittle 0001, Alan Bundy, Richard J. Boulton, Helen Lowe	System Description: CyNTHIA.	CADE	1999	DBLP DOI BibTeX RDF
27	Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury	Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems.	CADE	1999	DBLP DOI BibTeX RDF
27	Predrag Janicic, Alan Bundy, Ian Green	A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers.	CADE	1999	DBLP DOI BibTeX RDF
27	Raul H. C. Lopes	Automatic Generation of Proof Search Strategies for Second-order Logic.	CADE	1999	DBLP DOI BibTeX RDF
27	Andreas Franke 0001, Michael Kohlhase	System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.	CADE	1999	DBLP DOI BibTeX RDF
27	Tobias Nipkow	Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract).	CADE	1999	DBLP DOI BibTeX RDF
27	Carlos Areces, Hans de Nivelle, Maarten de Rijke	Prefixed Resolution: A Resolution Method for Modal and Description Logics.	CADE	1999	DBLP DOI BibTeX RDF
27	Viorica Sofronie-Stokkermans	On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results.	CADE	1999	DBLP DOI BibTeX RDF
27	Stephan Schulz 0001	System Abstract: E 0.3.	CADE	1999	DBLP DOI BibTeX RDF
27	Jason Hickey	Fault-Tolerant Distributed Theorem Proving.	CADE	1999	DBLP DOI BibTeX RDF
27	Erich Grädel	Invited Talk: Decision procedures for guarded logics.	CADE	1999	DBLP DOI BibTeX RDF
27	Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer	System Description: inka 5.0 - A Logic Voyager.	CADE	1999	DBLP DOI BibTeX RDF
27	Jian Zhang 0001	System Description: MCS: Model-based Conjecture Searching.	CADE	1999	DBLP DOI BibTeX RDF
27	Christoph Weidenbach	System Description: Spass Version 1.0.0.	CADE	1999	DBLP DOI BibTeX RDF
27	Christoph Weidenbach	Towards an Automatic Analysis of Security Protocols in First-Order Logic.	CADE	1999	DBLP DOI BibTeX RDF
27	E. Pascal Gribomont, Nachaat Salloum	System Description: Using OBDD's for the validation of Skolem verification conditions.	CADE	1999	DBLP DOI BibTeX RDF
27	Gopalan Nadathur, Dustin J. Mitchell	System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog.	CADE	1999	DBLP DOI BibTeX RDF
27	Stephan Tobies	A PSpace Algorithm for Graded Modal Logic.	CADE	1999	DBLP DOI BibTeX RDF
27	Thomas Hillenbrand, Andreas Jaeger, Bernd Löchner	System Description: Waldmeister - Improvements in Performance and Ease of Use.	CADE	1999	DBLP DOI BibTeX RDF
27	Manfred Schmidt-Schauß, Klaus U. Schulz	Solvability of Context Equations with Two Context Variables is Decidable.	CADE	1999	DBLP DOI BibTeX RDF
27	Tomasz Wierzbicki	Complexity of the higher order matching.	CADE	1999	DBLP DOI BibTeX RDF
27	Andrew A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin	VSDITLU: a verifiable symbolic definite integral table look-up.	CADE	1999	DBLP DOI BibTeX RDF
27	Frank Pfenning, Carsten Schürmann	System Description: Twelf - A Meta-Logical Framework for Deductive Systems.	CADE	1999	DBLP DOI BibTeX RDF
27	Marc Fuchs, Dirk Fuchs	Abstraction-Based Relevancy Testing for Model Elimination.	CADE	1999	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Norbert Eisinger, Ulrich Furbach	A Confluent Connection Calculus.	CADE	1999	DBLP DOI BibTeX RDF
27	Andrei Voronkov	KK: a theorem prover for K.	CADE	1999	DBLP DOI BibTeX RDF
27	Alexandre Riazanov, Andrei Voronkov	Vampire.	CADE	1999	DBLP DOI BibTeX RDF
27	Dieter Hutter, Alan Bundy	The Design of the CADE-16 Inductive Theorem Prover Contest.	CADE	1999	DBLP DOI BibTeX RDF
27	Matthew Bishop	A Breadth-First Strategy for Mating Search.	CADE	1999	DBLP DOI BibTeX RDF
27	Matthias Baaz, Alexander Leitsch, Georg Moser	System Description: CutRes 0.1: Cut Elimination by Resolution.	CADE	1999	DBLP DOI BibTeX RDF
27	Frédéric Prost	A formalization of Static Analyses in System F.	CADE	1999	DBLP DOI BibTeX RDF
27	Ullrich Hustadt, Renate A. Schmidt	Maslov's Class K Revisited.	CADE	1999	DBLP DOI BibTeX RDF
27	Sergei N. Artëmov	On Explicit Reflection in Theorem Proving and Formal Verification.	CADE	1999	DBLP DOI BibTeX RDF
27	Christoph Benzmüller	Extensional Higher-Order Paramodulation and RUE-Resolution.	CADE	1999	DBLP DOI BibTeX RDF
27	Helmut Horacek	Presenting Proofs in a Human-Oriented Way.	CADE	1999	DBLP DOI BibTeX RDF
27	Claude Kirchner, Hélène Kirchner (eds.)	Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings	CADE	1998	DBLP DOI BibTeX RDF
27	Grigore Rosu, Joseph A. Goguen	Hidden Congruent Deduction.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
27	Mark Hepple	Linear Categorial Deduction via First-order Compilation.	TAPD	1998	DBLP BibTeX RDF
27	Vítor Rocio, José Gabriel Lopes	Partial Parsing, Deduction and Tabling.	TAPD	1998	DBLP BibTeX RDF
27	Stéphane Fèvre, Dongming Wang 0001	Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules.	CADE	1998	DBLP DOI BibTeX RDF
27	Alexandre Boudet, Evelyne Contejean	About the Confluence of Equational Pattern Rewrite Systems.	CADE	1998	DBLP DOI BibTeX RDF
27	Frank Pfenning	Reasoning About Deductions in Linear Logic (Abstract of Invited Talk).	CADE	1998	DBLP DOI BibTeX RDF
27	Christoph Benzmüller, Michael Kohlhase	Extensional Higher-Order Resolution.	CADE	1998	DBLP DOI BibTeX RDF
27	Karl Crary	Admissibility of Fixpoint Induction over Partial Types.	CADE	1998	DBLP DOI BibTeX RDF
27	Bernhard Beckert, Rajeev Goré	System Description: leanK 2.0.	CADE	1998	DBLP DOI BibTeX RDF
27	Michael Beeson	Unification in Lambda-Calculi with if-then-else.	CADE	1998	DBLP DOI BibTeX RDF
27	Andreas Nonnengart, Georg Rock, Christoph Weidenbach	On Generating Small Clause Normal Forms.	CADE	1998	DBLP DOI BibTeX RDF
27	Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt	System Description: card TAP: The First Theorem Prover on a Smart Card.	CADE	1998	DBLP DOI BibTeX RDF
27	Tanel Tammet	Towards Efficient Subsumption.	CADE	1998	DBLP DOI BibTeX RDF
27	Jürgen Brauburger, Jürgen Giesl	Termination Analysis by Inductive Evaluation.	CADE	1998	DBLP DOI BibTeX RDF
27	Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa	On the Relationship Between Non-Horn Magic Sets and Relevancy Testing.	CADE	1998	DBLP DOI BibTeX RDF
27	Leo Bachmair, Harald Ganzinger, Andrei Voronkov	Elimination of Equality via Transformation with Ordering Constraints.	CADE	1998	DBLP DOI BibTeX RDF
27	Hans Jürgen Ohlbach	Combining Hilbert Style and Semantic Reasoning in a Resolution Framework.	CADE	1998	DBLP DOI BibTeX RDF
27	Thomas Arts, Mads Dam, Lars-Åke Fredlund, Dilian Gurov	System Description: Verification of Distributed Erlang Programs.	CADE	1998	DBLP DOI BibTeX RDF
27	Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy	System Description: An Interface Between CLAM and HOL.	CADE	1998	DBLP DOI BibTeX RDF
27	Julian Richardson, Alan Smaill, Ian Green	System Description: Proof Planning in Higher-Order Logic with Lambda-Clam.	CADE	1998	DBLP DOI BibTeX RDF
27	Matt Kaufmann	ACL2 Support for Verification Projects (Invited Talk).	CADE	1998	DBLP DOI BibTeX RDF
27	Uwe Waldmann	Superposition for Divisible Torsion-Free Abelian Groups.	CADE	1998	DBLP DOI BibTeX RDF
27	Nicolas Peltier	System Description: An Equational Constraints Solver.	CADE	1998	DBLP DOI BibTeX RDF
27	Bruno Pagano	X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi.	CADE	1998	DBLP DOI BibTeX RDF
27	Laurent Théry	A Certified Version of Buchberger's Algorithm.	CADE	1998	DBLP DOI BibTeX RDF
27	Joseph Douglas Horton, Bruce Spencer	Rank/Activity: A Canonical Form for Binary Resolution.	CADE	1998	DBLP DOI BibTeX RDF
27	Alberto Oliart, Wayne Snyder	A Fast Algorithm for Uniform Semi-Unification.	CADE	1998	DBLP DOI BibTeX RDF
27	Jacques D. Fleuriot, Lawrence C. Paulson	A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia.	CADE	1998	DBLP DOI BibTeX RDF
27	Bertrand Mazure, Lakhdar Sais, Éric Grégoire	System Description: CRIL Platform for SAT.	CADE	1998	DBLP DOI BibTeX RDF
27	Marc Fuchs, Andreas Wolf	System Description: Cooperation in Model Elimination: CPTHEO.	CADE	1998	DBLP DOI BibTeX RDF
27	Christoph Benzmüller, Michael Kohlhase	System Description: LEO - A Higher-Order Theorem Prover.	CADE	1998	DBLP DOI BibTeX RDF
27	Hans de Nivelle	A Resolution Decision Procedure for the Guarded Fragment.	CADE	1998	DBLP DOI BibTeX RDF
27	Leo Bachmair, Harald Ganzinger	Strict Basic Superposition.	CADE	1998	DBLP DOI BibTeX RDF
27	Marc Fuchs	System Description: Similarity-Based Lemma Generation for Model Elimination.	CADE	1998	DBLP DOI BibTeX RDF
27	Yannis Delmas-Rigoutsos	A Double Deduction System for Quantum Logic Based On Natural Deduction.	J. Philos. Log.	1997	DBLP DOI BibTeX RDF
27	William McCune (eds.)	Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings	CADE	1997	DBLP DOI BibTeX RDF
27	Wolfgang Bibel	Deduction as a Cross-Sectional Technology: The DFG Focus Programme on Deduction.	GI Jahrestagung	1997	DBLP DOI BibTeX RDF
27	Nicolas Peltier	Nouvelles techniques pour la construction de modèles finis ou infinis en déduction automatique. (New techniques for finite or infinite model building in automated deduction).		1997	RDF
27	Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier 0002, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge	Omega: Towards a Mathematical Assistant.	CADE	1997	DBLP DOI BibTeX RDF
27	Irène Durand, Aart Middeldorp	Decidable Call by Need Computations in term Rewriting (Extended Abstract).	CADE	1997	DBLP DOI BibTeX RDF