Search results for "CADE"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Robert S. Boyer	Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?	CADE	1994	DBLP DOI BibTeX RDF
1	Rolf Socher-Ambrosius	A Refined Version of General E-Unification.	CADE	1994	DBLP DOI BibTeX RDF
1	Jacques Chazarain, Emmanuel Kounalis	Mechanizable Inductive Proofs for a Class of Forall Exists Formulas.	CADE	1994	DBLP DOI BibTeX RDF
1	Jean Goubault	Proving with BDDs and Control of Information.	CADE	1994	DBLP DOI BibTeX RDF
1	Siani Baker	A New Application for Explanation-Based Generalisation within Automated Deduction.	CADE	1994	DBLP DOI BibTeX RDF
1	D. Andre de Waal, John P. Gallagher	The Applicability of Logic Program Analysis and Transformation to Theorem Proving.	CADE	1994	DBLP DOI BibTeX RDF
1	Koji Iwanuma	Conservative Query Normalization on Parallel Circumscription.	CADE	1994	DBLP DOI BibTeX RDF
1	Larry M. Hines	Str+ve and Integers.	CADE	1994	DBLP DOI BibTeX RDF
1	Takeshi Ohtani, Hajime Sawamura, Toshiro Minami	EUODHILOS-II on Top of GNU Epoch.	CADE	1994	DBLP DOI BibTeX RDF
1	Bernhard Beckert, Joachim Posegga	leanTAP: Lean Tableau-Based Theorem Proving (Extended Abstract).	CADE	1994	DBLP DOI BibTeX RDF
1	David A. Basin, Toby Walsh	Termination Orderings for Rippling.	CADE	1994	DBLP DOI BibTeX RDF
1	Lawrence C. Paulson	A Fixedpoint Approach to Implementing (Co)Inductive Definitions.	CADE	1994	DBLP DOI BibTeX RDF
1	Amy P. Felty, Douglas J. Howe	Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables.	CADE	1994	DBLP DOI BibTeX RDF
1	Christophe Bourely, Ricardo Caferra, Nicolas Peltier	A Method for Building Models Automatically. Experiments with an Extension of OTTER.	CADE	1994	DBLP DOI BibTeX RDF
1	Véronique Royer, Joachim Quantz	On Intuitionistic Query Answering in Description Bases.	CADE	1994	DBLP DOI BibTeX RDF	Intuitionistic Sequent Calculus, Least Fixed Point Semantics, Description Logics, Query Answering
1	Christian Prehofer	Decidable Higher-Order Unification Problems.	CADE	1994	DBLP DOI BibTeX RDF
1	Manfred Kerber, Michael Kohlhase	A Mechanization of Strong Kleene Logic for Partial Functions.	CADE	1994	DBLP DOI BibTeX RDF
1	Gernot Salzer	Primal Grammars and Unification Modulo a Binary Clause.	CADE	1994	DBLP DOI BibTeX RDF
1	Lars-Henrik Eriksson	Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions.	CADE	1994	DBLP DOI BibTeX RDF
1	Xiaorong Huang	Reconstruction Proofs at the Assertion Level.	CADE	1994	DBLP DOI BibTeX RDF
1	Claus-Peter Wirth, Bernhard Gramlich	On Notions of Inductive Validity for First-Oder Equational Clauses.	CADE	1994	DBLP DOI BibTeX RDF
1	Martin Protzen	Lazy Generation of Induction Hypotheses.	CADE	1994	DBLP DOI BibTeX RDF
1	Dongming Wang 0001	Algebraic Factoring and Geometry Proving.	CADE	1994	DBLP DOI BibTeX RDF
1	Ursula Martin	Termination, Geometry and Invariants.	CADE	1994	DBLP DOI BibTeX RDF
1	Johann Schumann	DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract.	CADE	1994	DBLP DOI BibTeX RDF
1	anonymous	The QED Manifesto.	CADE	1994	DBLP BibTeX RDF
1	Frederic D. Portoraro	Symlog: Automated Advice in Fitch-style Proof Construction.	CADE	1994	DBLP DOI BibTeX RDF
1	Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann	KEIM: A Toolkit for Automated Deduction.	CADE	1994	DBLP DOI BibTeX RDF
1	Maria Paola Bonacina, William McCune	Distributed Theorem Proving by Peers.	CADE	1994	DBLP DOI BibTeX RDF
1	Adel Bouhoula	SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs.	CADE	1994	DBLP DOI BibTeX RDF
1	Robert Nieuwenhuis, Albert Rubio	AC-Superposition with Constraints: No AC-Unifiers Needed.	CADE	1994	DBLP DOI BibTeX RDF
1	Fabio Massacci	Strongly Analytic Tableaux for Normal Modal Logics.	CADE	1994	DBLP DOI BibTeX RDF
1	Laurent Fribourg, Marcos Veloso Peixoto	Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints.	CADE	1994	DBLP DOI BibTeX RDF
1	Peter Baumgartner 0001, Ulrich Furbach	Model Elimination Without Contrapositives.	CADE	1994	DBLP DOI BibTeX RDF
1	William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer	Proof Script Pragmatics in IMPS.	CADE	1994	DBLP DOI BibTeX RDF
1	Patricia Johann, Michael Kohlhase	Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading.	CADE	1994	DBLP DOI BibTeX RDF
1	François Bronsard, Uday S. Reddy, Robert W. Hasker	Induction using Term Orderings.	CADE	1994	DBLP DOI BibTeX RDF
1	Toby Walsh	A Divergence Critic.	CADE	1994	DBLP DOI BibTeX RDF
1	Paul B. Jackson	Exploring Abstract Algebra in Constructive Type Theory.	CADE	1994	DBLP DOI BibTeX RDF
1	Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann	Omega-MKRP: A Proof Development Environment.	CADE	1994	DBLP DOI BibTeX RDF
1	Miki Hermann, Phokion G. Kolaitis	The Complexity of Counting Problems in Equational Matching.	CADE	1994	DBLP DOI BibTeX RDF
1	Tie-Cheng Wang, Allen Goldberg	KITP-93: An Automated Inference System for Program Analysis.	CADE	1994	DBLP DOI BibTeX RDF
1	Leo Bachmair, Harald Ganzinger	Ordered Chaining for Total Orderings.	CADE	1994	DBLP DOI BibTeX RDF
1	Aart Middeldorp, Hans Zantema	Simple Termination Revisited.	CADE	1994	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis	The TPTP Problem Library.	CADE	1994	DBLP DOI BibTeX RDF
1	Peter Baumgartner 0001, Ulrich Furbach	PROTEIN: A PROver with a Theory Extension INterface.	CADE	1994	DBLP DOI BibTeX RDF
1	David A. Plaisted	The Search Efficiency of Theorem Proving Strategies.	CADE	1994	DBLP DOI BibTeX RDF
1	John K. Slaney	FINDER: Finite Domain Enumerator - System Description.	CADE	1994	DBLP DOI BibTeX RDF
1	Richard Platek	What is a Proof? (Abstract).	CADE	1994	DBLP DOI BibTeX RDF
1	Stefan Brüning	Detecting Non-Provable Goals.	CADE	1994	DBLP DOI BibTeX RDF
1	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
1	Laurent Vigneron	Associative-Commutative Deduction with Constraints.	CADE	1994	DBLP DOI BibTeX RDF
1	Robert L. Constable	Exporting and Refecting Abstract Metamathematics.	CADE	1994	DBLP DOI BibTeX RDF
1	Nicholas Freitag McPhee, Shang-Ching Chou, Xiao-Shan Gao	Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method.	CADE	1994	DBLP DOI BibTeX RDF
1	Reinhard Bündgen	On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs.	CADE	1994	DBLP DOI BibTeX RDF
1	David B. Sturgill, Alberto Maria Segre	A Novel Asynchronous Parallelism Scheme for First-Order Logic.	CADE	1994	DBLP DOI BibTeX RDF
1	Stefan Klingenbeck, Reiner Hähnle	Semantic Tableaux with Ordering Restrictions.	CADE	1994	DBLP DOI BibTeX RDF
1	Bradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins	Mollusc: A General Proof-Development Shell for Sequent-Based Logics.	CADE	1994	DBLP DOI BibTeX RDF
1	Wolfgang Bibel, Stefan Brüning, Uwe Egly, Thomas Rath	KoMeT.	CADE	1994	DBLP DOI BibTeX RDF
1	Olaf Müller, Franz Weber	Theory and Practice of Minimal Modular Higher-Order E-Unification.	CADE	1994	DBLP DOI BibTeX RDF
1	John K. Slaney, Ewing L. Lusk, William McCune	SCOTT: Semantically Constrained Otter System Description.	CADE	1994	DBLP DOI BibTeX RDF
1	Dieter Hutter	Synthesis of Induction Orderings for Existence Proofs.	CADE	1994	DBLP DOI BibTeX RDF
1	Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood	Deductive Composition of Astronomical Software from Subroutine Libraries.	CADE	1994	DBLP DOI BibTeX RDF
1	Adam Cichon, Pierre Lescanne	Polynomial Interpretations and the Complexity of Algorithms.	CADE	1992	DBLP DOI BibTeX RDF
1	Shang-Ching Chou, Xiao-Shan Gao	Proving Geometry Statements of Constructive Type.	CADE	1992	DBLP DOI BibTeX RDF	Geometry theorem proving, Wu's method, non-degenerate condition, generally true, constructive geometry statement, metric geometry, algebraically closed field, Euclidean geometry
1	Kurt Ammon	Automatic Proofs in Mathematical Logic and Analysis.	CADE	1992	DBLP DOI BibTeX RDF
1	Tomás E. Uribe	Sorted Unification Using Set Constraints.	CADE	1992	DBLP DOI BibTeX RDF
1	Wolfgang Bibel, Steffen Hölldobler, Jörg Würtz	Cycle Unification.	CADE	1992	DBLP DOI BibTeX RDF
1	Franz Baader, Klaus U. Schulz	Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures.	CADE	1992	DBLP DOI BibTeX RDF
1	Zohar Manna, Richard J. Waldinger	The Special-Relation Rules are Incomplete.	CADE	1992	DBLP DOI BibTeX RDF
1	Deepak Kapur (eds.)	Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings	CADE	1992	DBLP DOI BibTeX RDF
1	Tie-Cheng Wang, Allen Goldberg	RVF: An Automated Formal Verification System.	CADE	1992	DBLP DOI BibTeX RDF
1	Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, Mark Saaltink	Eves System Description.	CADE	1992	DBLP DOI BibTeX RDF
1	Andrei Voronkov	Theorem Proving in Non-Standard Logics Based on the Inverse Method.	CADE	1992	DBLP DOI BibTeX RDF
1	Tobias Nipkow, Lawrence C. Paulson	Isabelle-91.	CADE	1992	DBLP DOI BibTeX RDF
1	Raymond M. Smullyan	Puzzles and Paradoxes (Abstract).	CADE	1992	DBLP DOI BibTeX RDF
1	Toby Walsh, Alex Nunes, Alan Bundy	The Use of Proof Plans to Sum Series.	CADE	1992	DBLP DOI BibTeX RDF
1	Wilfred Z. Chen	Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic.	CADE	1992	DBLP DOI BibTeX RDF
1	Xin Hua, Hantao Zhang 0001	FRI: Failure-Resistant Induction in RRL.	CADE	1992	DBLP DOI BibTeX RDF
1	Nachum Dershowitz, Subrata Mitra, G. Sivakumar	Decidable Matching for Convergent Systems (Preliminary Version).	CADE	1992	DBLP DOI BibTeX RDF
1	Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa	Embedding Negation as Failure into a Model Generation Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
1	Li Dafa	A Natural Deduction Automated Theorem Proving System.	CADE	1992	DBLP DOI BibTeX RDF
1	Larry M. Hines	The Central Variable Strategy of Str+ve.	CADE	1992	DBLP DOI BibTeX RDF
1	Larry Wos	The Impossibility of the Automation of Logical Reasoning.	CADE	1992	DBLP DOI BibTeX RDF
1	Geoffrey D. Alexander, David A. Plaisted	Proving Equality Theorems with Hyper-Linking.	CADE	1992	DBLP DOI BibTeX RDF
1	Ewing L. Lusk, Larry Wos	Benchmark Problems in Which Equality Plays the Major Role.	CADE	1992	DBLP DOI BibTeX RDF
1	Alan M. Frisch, Anthony G. Cohn 0001	An Abstract View of Sorted Unification.	CADE	1992	DBLP DOI BibTeX RDF
1	Michael Fisher 0001	A Normal Form for First-Order Temporal Formulae.	CADE	1992	DBLP DOI BibTeX RDF
1	Katherine A. Yelick, Stephen J. Garland	A Parallel Completion Procedure for Term Rewriting Systems.	CADE	1992	DBLP DOI BibTeX RDF
1	Mathias Bauer	An Interval-based Temporal Logic in a Multivalued Setting.	CADE	1992	DBLP DOI BibTeX RDF
1	Dave Barker-Plummer, Alex Rothenberg	The GAZER Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
1	Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig	The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics.	CADE	1992	DBLP DOI BibTeX RDF
1	Tobias Nipkow, Zhenyu Qian	Reduction and Unification in Lambda Calculi with Subtypes.	CADE	1992	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe	The Semantically Guided Linear Deduction System.	CADE	1992	DBLP DOI BibTeX RDF
1	Leonidas Fegaras, Tim Sheard, David W. Stemple	Uniform Traversal Combinators: Definition, Use and Properties.	CADE	1992	DBLP DOI BibTeX RDF
1	Ewing L. Lusk, William McCune, John K. Slaney	ROO: A Parallel Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
1	Tomás E. Uribe, Alan M. Frisch, Michael K. Mitchell	An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems.	CADE	1992	DBLP DOI BibTeX RDF
1	Natarajan Shankar	Proof Search in the Intuitionistic Sequent Calculus.	CADE	1992	DBLP DOI BibTeX RDF
1	Belaid Benhamou, Lakhdar Sais	Theoretical Study of Symmetries in Propositional Calculus and Applications.	CADE	1992	DBLP DOI BibTeX RDF
1	Sam Owre, John M. Rushby, Natarajan Shankar	PVS: A Prototype Verification System.	CADE	1992	DBLP DOI BibTeX RDF

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