Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
27	Gilles Défourneaux, Nicolas Peltier	Partial Matching for Analogy Discovery in Proofs and Counter-Examples.	CADE	1997	DBLP DOI BibTeX RDF
27	Andreas Wolf 0005, Johann Schumann	ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output.	CADE	1997	DBLP DOI BibTeX RDF
27	Moshe Y. Vardi	Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics.	CADE	1997	DBLP DOI BibTeX RDF
27	Daniel S. Korn, Christoph Kreitz	Deciding Intuitionistic Propositional Logic via Translation into Classical Logic.	CADE	1997	DBLP DOI BibTeX RDF
27	Johann Schumann	Automatic Verification of Cryptographic Protocols with SETHEO.	CADE	1997	DBLP DOI BibTeX RDF
27	Hantao Zhang 0001	SATO: An Efficient Propositional Prover.	CADE	1997	DBLP DOI BibTeX RDF
27	Jürgen Ehrensberger, Claus Zinn	DiaLog: A System for Dialogue Logic.	CADE	1997	DBLP DOI BibTeX RDF
27	Dirk Fuchs, Matthias Fuchs	CODE: A Powerful Prover for Problems of Condensed Detachment.	CADE	1997	DBLP DOI BibTeX RDF
27	Mary Cryan, Allan Ramsay	Constructing a Normal Form for Property Theory.	CADE	1997	DBLP DOI BibTeX RDF
27	Amy P. Felty, Douglas J. Howe	Hybrid Interactive Theorem Proving Using Nuprl and HOL.	CADE	1997	DBLP DOI BibTeX RDF
27	Jason J. Hickey	Nuprl-Light: An Implementation Framework for Higher-Order Logics.	CADE	1997	DBLP DOI BibTeX RDF
27	Uwe Egly	Some Pitfalls of LK-to-LJ Translations and How to Avoid Them.	CADE	1997	DBLP DOI BibTeX RDF
27	David von Oheimb, Thomas F. Gritzner	RALL: Machine-Supported Proofs for Relation Algebra.	CADE	1997	DBLP DOI BibTeX RDF	interactive and automatic theorem proving, atom structure, Relation algebra, Isabelle
27	Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe	A Practical Integration of First-Order Reasoning and Decision Procedures.	CADE	1997	DBLP DOI BibTeX RDF
27	Koji Iwanuma	Lemma Matching for a PTTP-based Top-down Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
27	Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani	A New Method for Testing Decision Procedures in Modal Logics.	CADE	1997	DBLP DOI BibTeX RDF
27	James Harland, David J. Pym	Resource-Distribution via Boolean Constraint (Extended Abstract).	CADE	1997	DBLP DOI BibTeX RDF
27	Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant	Proof Tactics for a Theory of State Machines in a Graphical Environment.	CADE	1997	DBLP DOI BibTeX RDF
27	Thomas Kolbe, Jürgen Brauburger	Plagiator - A Learning Prover.	CADE	1997	DBLP DOI BibTeX RDF
27	Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt	Connection-Based Proof Construction in Linear Logic.	CADE	1997	DBLP DOI BibTeX RDF
27	Dieter Hutter, Michael Kohlhase	A Colored Version of the Lambda-Calculus.	CADE	1997	DBLP DOI BibTeX RDF
27	Wu Wen-Tsün	The Char-Set Method and Its Applications to Automated Reasoning.	CADE	1997	DBLP DOI BibTeX RDF
27	Franz Baader, Cesare Tinelli	A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method.	CADE	1997	DBLP DOI BibTeX RDF
27	Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel	Proving System Correctness with KIV 3.0.	CADE	1997	DBLP DOI BibTeX RDF
27	John K. Slaney	Minlog: A Minimal Logic Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
27	Olivier Roussel, Philippe Mathieu	Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case.	CADE	1997	DBLP DOI BibTeX RDF
27	Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe	XIsabelle: A System Description.	CADE	1997	DBLP DOI BibTeX RDF
27	Seán Matthews	A Practical Implementation of Simple Consequence Relations Using Inductive Definitions.	CADE	1997	DBLP DOI BibTeX RDF
27	Bernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf	Integration of Automated and Interactive Theorem Proving in ILP.	CADE	1997	DBLP DOI BibTeX RDF
27	Richard Bornat, Bernard Sufrin	Jape: A Calculator for Animating Proof-on-Paper.	CADE	1997	DBLP DOI BibTeX RDF
27	Bernd Fischer 0002, Johann Schumann	SETHEO Goes Software Engineering: Application of ATP to Software Reuse.	CADE	1997	DBLP DOI BibTeX RDF
27	Helen Lowe, David Duncan	XBarnacle: Making Theorem Provers More Accessible.	CADE	1997	DBLP DOI BibTeX RDF
27	Joachim Niehren, Manfred Pinkal, Peter Ruhrberg	On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting.	CADE	1997	DBLP DOI BibTeX RDF	tree constraints, subtree relation, string unification, context unification, linear second-order unification, one-step rewriting, semantic processing of natural language
27	Lu Yang, Hongguang Fu, Zhenbing Zeng	A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry.	CADE	1997	DBLP DOI BibTeX RDF
27	Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura	Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving.	CADE	1997	DBLP DOI BibTeX RDF
27	Hans de Nivelle	A Classification of Non-liftable Orders for Resolution.	CADE	1997	DBLP DOI BibTeX RDF
27	Harald Ganzinger, Christoph Meyer 0001, Christoph Weidenbach	Soft Typing for Ordered Resolution.	CADE	1997	DBLP DOI BibTeX RDF
27	Mathias Kettner, Norbert Eisinger	The Tableau Browser SNARKS.	CADE	1997	DBLP DOI BibTeX RDF
27	Louise A. Dennis, Alan Bundy, Ian Green	Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs.	CADE	1997	DBLP DOI BibTeX RDF
27	Michael A. McRobbie, John K. Slaney (eds.)	Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings	CADE	1996	DBLP DOI BibTeX RDF
27	Sergei G. Vorobyov	An Improved Lower Bound for the Elementary Theories of Trees.	CADE	1996	DBLP DOI BibTeX RDF
27	Andrew Ireland, Alan Bundy	Extensions to a Generalization Critic for Inductive Proof.	CADE	1996	DBLP DOI BibTeX RDF
27	Qing Guo, Paliath Narendran, David A. Wolfram	Unification and Matching Modulo Nilpotence.	CADE	1996	DBLP DOI BibTeX RDF	Subject area MECHANISMS, unification
27	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
27	Thierry Boy de la Tour	Ground Resolution with Group Computations on Semantic Symmetries.	CADE	1996	DBLP DOI BibTeX RDF
27	Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema	Transforming Termination by Self-Labelling.	CADE	1996	DBLP DOI BibTeX RDF
27	Christian B. Suttner, Geoff Sutcliffe	The Design of the CADE-13 ATP System Competition.	CADE	1996	DBLP DOI BibTeX RDF
27	Thomas Kolbe, Christoph Walther	Termination of Theorem Proving by Reuse.	CADE	1996	DBLP DOI BibTeX RDF
27	Heribert Schütz, Tim Geisler	Efficient Model Generation through Compilation.	CADE	1996	DBLP DOI BibTeX RDF
27	Giovanni Felici, Giovanni Rinaldi, Klaus Truemper	FasTraC: A Decentralized Traffic Control System Based on Logic Programming.	CADE	1996	DBLP DOI BibTeX RDF
27	Erica Melis, Jon Whittle 0001	Internal Analogy in Theorem Proving.	CADE	1996	DBLP DOI BibTeX RDF
27	Konstantinos Sagonas, Terrance Swift, David Scott Warren	An Abstract Machine for Fixed-Order Dynamically Stratified Programs.	CADE	1996	DBLP DOI BibTeX RDF
27	Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang	An Introduction to Geometry Expert.	CADE	1996	DBLP DOI BibTeX RDF
27	Andrei Voronkov	Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.	CADE	1996	DBLP DOI BibTeX RDF
27	Martin Protzen	Patching Faulty Conjectures.	CADE	1996	DBLP DOI BibTeX RDF
27	David Cyrluk, Patrick Lincoln, Natarajan Shankar	On Shostak's Decision Procedure for Combinations of Theories.	CADE	1996	DBLP DOI BibTeX RDF
27	Dieter Hutter, Claus Sengler	INKA: The Next Generation.	CADE	1996	DBLP DOI BibTeX RDF
27	Hans Jürgen Ohlbach	SCAN - Elimination of Predicate Quantifiers.	CADE	1996	DBLP DOI BibTeX RDF
27	Christoph Weidenbach, Bernd Gaede, Georg Rock	SPASS & FLOTTER Version 0.42.	CADE	1996	DBLP DOI BibTeX RDF
27	Tanel Tammet	A Resolution Theorem Prover for Intuitonistic Logic.	CADE	1996	DBLP DOI BibTeX RDF
27	Stephan Schmitt, Christoph Kreitz	Converting Non-Classical Matrix Proofs into Sequent-Style Systems.	CADE	1996	DBLP DOI BibTeX RDF
27	Peter Graf, Christoph Meyer 0001	Advanced Indexing Operations on Substitution Trees.	CADE	1996	DBLP DOI BibTeX RDF
27	Amy P. Felty	Proof Search with Set Variable Instantiation in the Calculus of Constructions.	CADE	1996	DBLP DOI BibTeX RDF
27	Janet Bertot, Yves Bertot	CtCoq: A System Presentation.	CADE	1996	DBLP DOI BibTeX RDF	system presentation, Application
27	William M. Farmer, Joshua D. Guttman, F. Javier Thayer	IMPS: An Updated System Description.	CADE	1996	DBLP DOI BibTeX RDF
27	Torsten Schaub, Stefan Brüning, Pascal Nicolas	XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description.	CADE	1996	DBLP DOI BibTeX RDF
27	Fausto Giunchiglia, Roberto Sebastiani	Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K.	CADE	1996	DBLP DOI BibTeX RDF
27	Peter V. Homeier, David F. Martin	Mechanical Verification of Mutually Recursive Procedures.	CADE	1996	DBLP DOI BibTeX RDF
27	Jian Zhang 0001, Hantao Zhang 0001	System Description: Generating Models by SEM.	CADE	1996	DBLP DOI BibTeX RDF
27	Uwe Egly, Thomas Rath	On the Practical Value of Different Definitional Translations to Normal Form.	CADE	1996	DBLP DOI BibTeX RDF
27	John Harrison 0001	Optimizing Proof Search in Model Elimination.	CADE	1996	DBLP DOI BibTeX RDF
27	Tai Joon Park, Allen Van Gelder	Partitioning Methods for Satisfiability Testing on Large Formulas.	CADE	1996	DBLP DOI BibTeX RDF
27	Giuseppe De Giacomo, Fabio Massacci	Tableaux and Algorithms for Propositional Dynamic Logic with Converse.	CADE	1996	DBLP DOI BibTeX RDF
27	Harald Ganzinger, Uwe Waldmann	Theorem Proving in Cancellative Abelian Monoids (Extended Abstract).	CADE	1996	DBLP DOI BibTeX RDF
27	Claus Sengler	Termination of Algorithms over Non-freely Generated Data Types.	CADE	1996	DBLP DOI BibTeX RDF
27	Dongming Wang 0001	GEOTHER: A Geometry Theorem Prover.	CADE	1996	DBLP DOI BibTeX RDF
27	Harald Ganzinger	Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract).	CADE	1996	DBLP DOI BibTeX RDF
27	Christian G. Fermüller	Semantic Trees Revisited: Some New Completeness Results.	CADE	1996	DBLP DOI BibTeX RDF
27	Miki Hermann, Phokion G. Kolaitis	Unification Algorithms Cannot be Combined in Polynomial Time.	CADE	1996	DBLP DOI BibTeX RDF
27	Andreas Nonnengart	Resolution-Based Calculi for Modal and Temporal Logics.	CADE	1996	DBLP DOI BibTeX RDF
27	Christoph Weidenbach	Unification in Pseudo-Linear Sort Theories is Decidable.	CADE	1996	DBLP DOI BibTeX RDF
27	Olivier Roussel, Philippe Mathieu	A New Method for Knowledge Compilation: The Achievement by Cycle Search.	CADE	1996	DBLP DOI BibTeX RDF	expert systems, resolution, knowledge compilation
27	Ursula Martin	Theorem Proving with Group Presentations: Examples and Questions.	CADE	1996	DBLP DOI BibTeX RDF
27	Deepak Kapur, Mahadevan Subramaniam	Lemma Discovery in Automated Induction.	CADE	1996	DBLP DOI BibTeX RDF
27	Harald Rueß	Reflection of Formal Tactics in a Deductive Reflection Framework.	CADE	1996	DBLP DOI BibTeX RDF
27	Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann	The Tableau-based Theorem Prover 3TAP Version 4.0.	CADE	1996	DBLP DOI BibTeX RDF
27	Johann Schumann	SiCoTHEO: Simple Competitive Parallel Theorem Provers.	CADE	1996	DBLP DOI BibTeX RDF
27	Fausto Giunchiglia, Adolfo Villafiorita	ABSFOL: A Proof Checker with Abstraction.	CADE	1996	DBLP DOI BibTeX RDF
27	Clare Dixon	Search Strategies for Resolution in Temporal Logics.	CADE	1996	DBLP DOI BibTeX RDF
27	Eike Ritter, David J. Pym, Lincoln A. Wallen	Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract).	CADE	1996	DBLP DOI BibTeX RDF
27	Ole Rasmussen	An Embedding of Ruby in Isabelle.	CADE	1996	DBLP DOI BibTeX RDF
27	David A. McAllester, Kostas Arkoudas	Walther Recursion.	CADE	1996	DBLP DOI BibTeX RDF
27	Alan Bundy (eds.)	Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings	CADE	1994	DBLP DOI BibTeX RDF
27	Laurent Vigneron	Déduction automatique avec contraintes symboliques dans les théories équationnelles. (Automated deduction with symbolic constraints in equational theories).		1994	RDF
27	Eric Domenjoud, Francis Klay, Christophe Ringeissen	Combination Techniques for Non-Disjoint Equational Theories.	CADE	1994	DBLP DOI BibTeX RDF
27	Penny Anderson	Representing Proof Transformations for Program Optimizations.	CADE	1994	DBLP DOI BibTeX RDF
27	Jian Zhang 0001	Problems on the Generation of Finite Models.	CADE	1994	DBLP DOI BibTeX RDF
27	John K. Slaney	The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure.	CADE	1994	DBLP DOI BibTeX RDF
27	Edmund M. Clarke, Xudong Zhao 0005	Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan.	CADE	1994	DBLP DOI BibTeX RDF
27	Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann	SETHEO V3.2: Recent Developments - System Abstract.	CADE	1994	DBLP DOI BibTeX RDF