Search results for "CADE"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Martin Protzen	Disproving Conjectures.	CADE	1992	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe	Linear-Input Subset Analysis.	CADE	1992	DBLP DOI BibTeX RDF
1	K. Blackburn	A Report in ICL HOL.	CADE	1992	DBLP DOI BibTeX RDF
1	Shang-Ching Chou	A Geometry Theorem Prover for Macintoshes.	CADE	1992	DBLP DOI BibTeX RDF
1	Daniel J. Dougherty, Patricia Johann	A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract).	CADE	1992	DBLP DOI BibTeX RDF
1	David A. Randell, Anthony G. Cohn 0001, Zhan Cui	Computing Transivity Tables: A Challenge For Automated Theorem Provers.	CADE	1992	DBLP DOI BibTeX RDF
1	Hantao Zhang 0001	Herky: High Performance Rewriting in RRL.	CADE	1992	DBLP DOI BibTeX RDF
1	Wolfgang Reif	The KIV System: Systematic Construction of Verified Software.	CADE	1992	DBLP DOI BibTeX RDF
1	Owen L. Astrachan, Mark E. Stickel	Caching and Lemmaizing in Model Elimination Theorem Provers.	CADE	1992	DBLP DOI BibTeX RDF
1	Jim Christian	Some Termination Criteria for Narrowing and E-Narrowing.	CADE	1992	DBLP DOI BibTeX RDF
1	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	The FAUST - Prover.	CADE	1992	DBLP DOI BibTeX RDF
1	Peter Madden	Automatic Program Optimization Through Proof Transformation.	CADE	1992	DBLP DOI BibTeX RDF
1	Peter Jackson	Computing Prime Implicates Incrementally.	CADE	1992	DBLP DOI BibTeX RDF
1	Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder	Basic Paramodulation and Superposition.	CADE	1992	DBLP DOI BibTeX RDF
1	William M. Farmer, Joshua D. Guttman, F. Javier Thayer	IMPS: System Description.	CADE	1992	DBLP DOI BibTeX RDF
1	Ricardo Caferra, Stéphane Demri	Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic.	CADE	1992	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Xudong Zhao 0005	Analytica - A Theorem Prover in Mathematica.	CADE	1992	DBLP DOI BibTeX RDF
1	Alexandre Boudet	Unification in Order-Sorted Algebras with Overloading.	CADE	1992	DBLP DOI BibTeX RDF
1	R. C. Sekar 0001, I. V. Ramakrishnan	Programming with Equations: A Framework for Lazy Parallel Evaluation.	CADE	1992	DBLP DOI BibTeX RDF
1	Delia Kesner	Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors.	CADE	1992	DBLP DOI BibTeX RDF
1	Kurt Ammon	The SHUNYATA System.	CADE	1992	DBLP DOI BibTeX RDF
1	Hantao Zhang 0001, Xin Hua	Proving the Chinese Remainder Theorem by the Cover Set Induction.	CADE	1992	DBLP DOI BibTeX RDF
1	Robert Nieuwenhuis, Albert Rubio	Theorem Proving with Ordering Constrained Clauses.	CADE	1992	DBLP DOI BibTeX RDF
1	William M. Farmer, Joshua D. Guttman, F. Javier Thayer	Little Theories.	CADE	1992	DBLP DOI BibTeX RDF
1	William McCune, Larry Wos	Experiments in Automated Deduction with Condensed Detachment.	CADE	1992	DBLP DOI BibTeX RDF
1	Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill	&: Automated Natural Deduction.	CADE	1992	DBLP DOI BibTeX RDF
1	Vincent J. Digricoli, Eugene Kochendorfer	LIM+ Challenge Problems by RUE Hyper-Resolution.	CADE	1992	DBLP DOI BibTeX RDF
1	Konstantin Vershinin, Igor Romanenko	One More Logic with Uncertainty and Resolution Principle for it.	CADE	1992	DBLP DOI BibTeX RDF
1	Anthony G. Cohn 0001	A Many Sorted Logic with Possibly Empty Sorts.	CADE	1992	DBLP DOI BibTeX RDF
1	Bernhard Beckert, Reiner Hähnle	An Improved Method for Adding Equality to Free Variable Semantic Tableaux.	CADE	1992	DBLP DOI BibTeX RDF
1	David A. Basin, Toby Walsh	Difference Matching.	CADE	1992	DBLP DOI BibTeX RDF
1	Frank Pfenning, Ekkehard Rohwedder	Implementing the Meta-Theory of Deductive Systems.	CADE	1992	DBLP DOI BibTeX RDF
1	Robert S. Boyer, Yuan Yu	Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor.	CADE	1992	DBLP DOI BibTeX RDF	Nqthm, Boyer-Moore Theorem Prover, Gnu, Ada, C, Automated reasoning, object code, formal program verification
1	Jawahar Chirimar, Carl A. Gunter, Myra Van Inwegen	Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker.	CADE	1992	DBLP DOI BibTeX RDF
1	David A. McAllester	Grammar Rewriting.	CADE	1992	DBLP DOI BibTeX RDF
1	Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita 0002	MGTP: A Parallel Theorem Prover Based on Lazy Model Generation.	CADE	1992	DBLP DOI BibTeX RDF
1	Jane Hesketh, Alan Bundy, Alan Smaill	Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs.	CADE	1992	DBLP DOI BibTeX RDF
1	Johann Schumann	KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract).	CADE	1992	DBLP DOI BibTeX RDF
1	Maritta Heisel, Wolfgang Reif, Werner Stephan 0001	Tactical Theorem Proving in Program Verification.	CADE	1990	DBLP DOI BibTeX RDF
1	Dieter Hutter	Guiding Induction Proofs.	CADE	1990	DBLP DOI BibTeX RDF
1	Johann Schumann, Reinhold Letz, Franz J. Kurfess	Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation.	CADE	1990	DBLP DOI BibTeX RDF
1	Paul Pritchard, John K. Slaney	Tutorial on Computing Models of Propositional Logics.	CADE	1990	DBLP DOI BibTeX RDF
1	John K. Slaney, Ewing L. Lusk	Parallelizing the Closure Computation in Automated Deduction.	CADE	1990	DBLP DOI BibTeX RDF
1	Neil V. Murray, Erik Rosenthal	DISSOLVER: A Dissolution-based Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
1	Frank Pfenning, Dan Nesmith	Presenting Intuitive Deductions via Symmetric Simplification.	CADE	1990	DBLP DOI BibTeX RDF
1	Ralph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek	A High-Performance Parallel Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
1	John L. Pollock	OSCAR.	CADE	1990	DBLP DOI BibTeX RDF
1	Jürgen Müller 0008, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka	Tutorial on Reasoning and Representation with Concept Languages.	CADE	1990	DBLP DOI BibTeX RDF
1	Toshiro Wakayama, T. H. Payne	Case-Free Programs: An Abstraction of Definite Horn Programs.	CADE	1990	DBLP DOI BibTeX RDF
1	Dan Benanav	Simultaneous Paramodulation.	CADE	1990	DBLP DOI BibTeX RDF
1	Matt Kaufmann	RCL: A Lisp Verification System.	CADE	1990	DBLP DOI BibTeX RDF
1	Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian	Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation.	CADE	1990	DBLP DOI BibTeX RDF
1	Frank M. Brown, Carlos Araya	Cylindric Algebra Equation Solver.	CADE	1990	DBLP DOI BibTeX RDF
1	Shang-Ching Chou, Xiao-Shan Gao	Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving.	CADE	1990	DBLP DOI BibTeX RDF	Wu's method, prover, elementary geometry, degenerate conditions, Ritt-Wu's principle, ascending chain, the dimension theorem, Morley's trisector theorem, ideal, mechanical theorem proving, algebraic variety
1	Amy P. Felty, Dale Miller 0001	Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language.	CADE	1990	DBLP DOI BibTeX RDF
1	Christian B. Suttner, Wolfgang Ertel	Automatic Acquisition of Search Guiding Heuristics.	CADE	1990	DBLP DOI BibTeX RDF	learning, heuristics, features, Automated theorem proving, back-propagation, connectionism, evaluation functions, model elimination
1	Mark E. Stickel	A Prolog Technology Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
1	Frank M. Brown, Carlos Araya	Schemata.	CADE	1990	DBLP DOI BibTeX RDF
1	Alan Bundy, Frank van Harmelen, Alan Smaill, Andrew Ireland	Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs.	CADE	1990	DBLP DOI BibTeX RDF
1	Wayne Snyder	Higher Order E-Unification.	CADE	1990	DBLP DOI BibTeX RDF
1	Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler	Automated Reasoning Contributed to Mathematics and Logic.	CADE	1990	DBLP DOI BibTeX RDF
1	Alexandre Boudet	Unification in a Combination of Equational Theories: an Efficient Algorithm.	CADE	1990	DBLP DOI BibTeX RDF
1	Thierry Boy de la Tour	Minimizing the Number of Clauses by Renaming.	CADE	1990	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe	A General Clause Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
1	Ursula Martin, Tobias Nipkow	Ordered Rewriting and Confluence.	CADE	1990	DBLP DOI BibTeX RDF
1	David A. Wolfram	ACE: The Abstract Clause Engine.	CADE	1990	DBLP DOI BibTeX RDF
1	Alan Bundy	A Science of Reasoning: Extended Abstract.	CADE	1990	DBLP DOI BibTeX RDF
1	Andrei Voronkov	LISS - The Logic Inference Search System.	CADE	1990	DBLP DOI BibTeX RDF
1	Leo Bachmair, Harald Ganzinger	On Restrictions of Ordered Paramodulation with Simplification.	CADE	1990	DBLP DOI BibTeX RDF
1	Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning	The TPS Theorem Proving System.	CADE	1990	DBLP DOI BibTeX RDF
1	Chitta Baral, Jorge Lobo 0001, Jack Minker	Generalized Well-founded Semantics for Logic Programs (Extended Abstract).	CADE	1990	DBLP DOI BibTeX RDF
1	Jieh Hsiang, Jean-Pierre Jouannaud	Tutorial on Rewrite-Based Theorem Proving.	CADE	1990	DBLP DOI BibTeX RDF
1	Pierre Lescanne	ORME: An Implementation of Completion Procedures as Sets of Transition Rules.	CADE	1990	DBLP DOI BibTeX RDF
1	William M. Farmer, Joshua D. Guttman, F. Javier Thayer	IMPS: An Interactive Mathematical Proof System.	CADE	1990	DBLP DOI BibTeX RDF
1	Wolfgang Bibel	Perspectives on Automated Deduction (Abstract).	CADE	1990	DBLP DOI BibTeX RDF
1	Carl Eichenlaub, Bruce Esrig, James Hook, Carl Klapper, Garrel Pottinger	The Romulus Proof Checker.	CADE	1990	DBLP DOI BibTeX RDF
1	Yusuf Ozturk, Lawrence J. Henschen	Hyper Resolution and Equality Axioms without Function Substitutions.	CADE	1990	DBLP DOI BibTeX RDF
1	Sang Ho Lee, Lawrence J. Henschen	Substitution-based Compilation of Extended Rules in Deductive Databases.	CADE	1990	DBLP DOI BibTeX RDF
1	Masami Hagiya	Programming by Example and Proving by Example Using Higher-order Unification.	CADE	1990	DBLP DOI BibTeX RDF
1	Gerald E. Peterson	Complete Sets of Reductions with Constraints.	CADE	1990	DBLP DOI BibTeX RDF
1	Bernhard Gramlich	UNICOM: A Refined Completion Based Inductive Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
1	Mikael Rittri	Retrieving Library Identifiers via Equational Matching of Types.	CADE	1990	DBLP DOI BibTeX RDF
1	William Pierce	Toward Mechanical Methods for Streamlining Proofs.	CADE	1990	DBLP DOI BibTeX RDF
1	Robert Nieuwenhuis, Fernando Orejas, Albert Rubio	TRIP: An Implementation of Clausal Rewriting.	CADE	1990	DBLP DOI BibTeX RDF
1	Larry M. Hines	Str+ve-Subset: The Str+ve-based Subset Prover.	CADE	1990	DBLP DOI BibTeX RDF
1	David A. Basin	Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete.	CADE	1990	DBLP DOI BibTeX RDF
1	Amy P. Felty, Elsa L. Gunter, Dale Miller 0001, Frank Pfenning	Tutorial on Lambda-Prolog.	CADE	1990	DBLP DOI BibTeX RDF
1	Hans-Jürgen Bürckert	A Resolution Principle for Clauses with Constraints.	CADE	1990	DBLP DOI BibTeX RDF
1	Uday S. Reddy	Term Rewriting Induction.	CADE	1990	DBLP DOI BibTeX RDF
1	Joachim Steinbach	Improving Assoviative Path Orderings.	CADE	1990	DBLP DOI BibTeX RDF
1	William McCune	OTTER 2.0.	CADE	1990	DBLP DOI BibTeX RDF
1	Robert S. Boyer, J Strother Moore	A Theorem Prover for a Computational Logic.	CADE	1990	DBLP DOI BibTeX RDF
1	Mark E. Stickel (eds.)	10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings	CADE	1990	DBLP DOI BibTeX RDF
1	Ewing L. Lusk, William McCune	Tutorial on High-Performance Automated Theorem Proving.	CADE	1990	DBLP DOI BibTeX RDF
1	Heikki Tuominen	Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic.	CADE	1990	DBLP DOI BibTeX RDF
1	David J. Pym, Lincoln A. Wallen	Investigations into Proof-Search in a System of First-Order Dependent Function Types.	CADE	1990	DBLP DOI BibTeX RDF
1	Richard J. Waldinger	Tutorial on Program-Synthetic Deduction.	CADE	1990	DBLP DOI BibTeX RDF
1	Hans Jürgen Ohlbach, Andreas Herzig	Tutorial on Compilation techniques for Logics.	CADE	1990	DBLP DOI BibTeX RDF
1	Alan F. McMichael	SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory.	CADE	1990	DBLP DOI BibTeX RDF
1	Daniel J. Dougherty, Patricia Johann	An Improved General E-Unification Method.	CADE	1990	DBLP DOI BibTeX RDF

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