Search results for "CADE"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	James Harland, David J. Pym	Resource-Distribution via Boolean Constraint (Extended Abstract).	CADE	1997	DBLP DOI BibTeX RDF
1	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
1	Thomas Kolbe, Jürgen Brauburger	Plagiator - A Learning Prover.	CADE	1997	DBLP DOI BibTeX RDF
1	Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt	Connection-Based Proof Construction in Linear Logic.	CADE	1997	DBLP DOI BibTeX RDF
1	Dieter Hutter, Michael Kohlhase	A Colored Version of the Lambda-Calculus.	CADE	1997	DBLP DOI BibTeX RDF
1	Wu Wen-Tsün	The Char-Set Method and Its Applications to Automated Reasoning.	CADE	1997	DBLP DOI BibTeX RDF
1	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
1	Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel	Proving System Correctness with KIV 3.0.	CADE	1997	DBLP DOI BibTeX RDF
1	John K. Slaney	Minlog: A Minimal Logic Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
1	Olivier Roussel, Philippe Mathieu	Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case.	CADE	1997	DBLP DOI BibTeX RDF
1	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
1	Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe	XIsabelle: A System Description.	CADE	1997	DBLP DOI BibTeX RDF
1	Seán Matthews	A Practical Implementation of Simple Consequence Relations Using Inductive Definitions.	CADE	1997	DBLP DOI BibTeX RDF
1	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
1	Richard Bornat, Bernard Sufrin	Jape: A Calculator for Animating Proof-on-Paper.	CADE	1997	DBLP DOI BibTeX RDF
1	Maria Paola Bonacina	The Clause-Diffusion Theorem Prover Peers-mcd (System Description).	CADE	1997	DBLP DOI BibTeX RDF
1	Bernd Fischer 0002, Johann Schumann	SETHEO Goes Software Engineering: Application of ATP to Software Reuse.	CADE	1997	DBLP DOI BibTeX RDF
1	Helen Lowe, David Duncan	XBarnacle: Making Theorem Provers More Accessible.	CADE	1997	DBLP DOI BibTeX RDF
1	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
1	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
1	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
1	Hans de Nivelle	A Classification of Non-liftable Orders for Resolution.	CADE	1997	DBLP DOI BibTeX RDF
1	Harald Ganzinger, Christoph Meyer 0001, Christoph Weidenbach	Soft Typing for Ordered Resolution.	CADE	1997	DBLP DOI BibTeX RDF
1	Mathias Kettner, Norbert Eisinger	The Tableau Browser SNARKS.	CADE	1997	DBLP DOI BibTeX RDF
1	Louise A. Dennis, Alan Bundy, Ian Green	Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs.	CADE	1997	DBLP DOI BibTeX RDF
1	Sergei G. Vorobyov	An Improved Lower Bound for the Elementary Theories of Trees.	CADE	1996	DBLP DOI BibTeX RDF
1	Andrew Ireland, Alan Bundy	Extensions to a Generalization Critic for Inductive Proof.	CADE	1996	DBLP DOI BibTeX RDF
1	Qing Guo, Paliath Narendran, David A. Wolfram	Unification and Matching Modulo Nilpotence.	CADE	1996	DBLP DOI BibTeX RDF	Subject area MECHANISMS, unification
1	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
1	Thierry Boy de la Tour	Ground Resolution with Group Computations on Semantic Symmetries.	CADE	1996	DBLP DOI BibTeX RDF
1	Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema	Transforming Termination by Self-Labelling.	CADE	1996	DBLP DOI BibTeX RDF
1	Saturnino F. Luz-Filho	Grammar Specification in Categorial Logics and Theorem Proving.	CADE	1996	DBLP DOI BibTeX RDF	Mechanisms (semantic tableaux) and Applications (computational liguistics)
1	Peter Graf	Path Indexing for AC-Theories.	CADE	1996	DBLP DOI BibTeX RDF
1	Christian B. Suttner, Geoff Sutcliffe	The Design of the CADE-13 ATP System Competition.	CADE	1996	DBLP DOI BibTeX RDF
1	Thomas Kolbe, Christoph Walther	Termination of Theorem Proving by Reuse.	CADE	1996	DBLP DOI BibTeX RDF
1	Wayne Snyder, James G. Schmolze	Rewrite Semantics for Production Rule Systems: Theory and Applications.	CADE	1996	DBLP DOI BibTeX RDF
1	Heribert Schütz, Tim Geisler	Efficient Model Generation through Compilation.	CADE	1996	DBLP DOI BibTeX RDF
1	Dana S. Scott	What Can We Hope to Achieve From Automated Deduction? (Abstract).	CADE	1996	DBLP DOI BibTeX RDF
1	Giovanni Felici, Giovanni Rinaldi, Klaus Truemper	FasTraC: A Decentralized Traffic Control System Based on Logic Programming.	CADE	1996	DBLP DOI BibTeX RDF
1	Erica Melis, Jon Whittle 0001	Internal Analogy in Theorem Proving.	CADE	1996	DBLP DOI BibTeX RDF
1	Konstantinos Sagonas, Terrance Swift, David Scott Warren	An Abstract Machine for Fixed-Order Dynamically Stratified Programs.	CADE	1996	DBLP DOI BibTeX RDF
1	Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang	An Introduction to Geometry Expert.	CADE	1996	DBLP DOI BibTeX RDF
1	Andrei Voronkov	Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.	CADE	1996	DBLP DOI BibTeX RDF
1	Martin Protzen	Patching Faulty Conjectures.	CADE	1996	DBLP DOI BibTeX RDF
1	David Cyrluk, Patrick Lincoln, Natarajan Shankar	On Shostak's Decision Procedure for Combinations of Theories.	CADE	1996	DBLP DOI BibTeX RDF
1	Dieter Hutter, Claus Sengler	INKA: The Next Generation.	CADE	1996	DBLP DOI BibTeX RDF
1	Hans Jürgen Ohlbach	SCAN - Elimination of Predicate Quantifiers.	CADE	1996	DBLP DOI BibTeX RDF
1	Christoph Weidenbach, Bernd Gaede, Georg Rock	SPASS & FLOTTER Version 0.42.	CADE	1996	DBLP DOI BibTeX RDF
1	Tanel Tammet	A Resolution Theorem Prover for Intuitonistic Logic.	CADE	1996	DBLP DOI BibTeX RDF
1	Xiaorong Huang, Armin Fiedler	Presenting Machine-Found Proofs.	CADE	1996	DBLP DOI BibTeX RDF
1	Gernot Salzer	Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices.	CADE	1996	DBLP DOI BibTeX RDF
1	Stephan Schmitt, Christoph Kreitz	Converting Non-Classical Matrix Proofs into Sequent-Style Systems.	CADE	1996	DBLP DOI BibTeX RDF
1	Peter Graf, Christoph Meyer 0001	Advanced Indexing Operations on Substitution Trees.	CADE	1996	DBLP DOI BibTeX RDF
1	Amy P. Felty	Proof Search with Set Variable Instantiation in the Calculus of Constructions.	CADE	1996	DBLP DOI BibTeX RDF
1	Janet Bertot, Yves Bertot	CtCoq: A System Presentation.	CADE	1996	DBLP DOI BibTeX RDF	system presentation, Application
1	William M. Farmer, Joshua D. Guttman, F. Javier Thayer	IMPS: An Updated System Description.	CADE	1996	DBLP DOI BibTeX RDF
1	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
1	Matthias Fuchs	Experiments in the Heuristic Use of Past Proof Experience.	CADE	1996	DBLP DOI BibTeX RDF
1	David A. Basin, Seán Matthews	Structuring Metatheory on Inductive Definitions.	CADE	1996	DBLP DOI BibTeX RDF
1	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
1	Peter V. Homeier, David F. Martin	Mechanical Verification of Mutually Recursive Procedures.	CADE	1996	DBLP DOI BibTeX RDF
1	Jian Zhang 0001, Hantao Zhang 0001	System Description: Generating Models by SEM.	CADE	1996	DBLP DOI BibTeX RDF
1	Uwe Egly, Thomas Rath	On the Practical Value of Different Definitional Translations to Normal Form.	CADE	1996	DBLP DOI BibTeX RDF
1	John Harrison 0001	Optimizing Proof Search in Model Elimination.	CADE	1996	DBLP DOI BibTeX RDF
1	Tai Joon Park, Allen Van Gelder	Partitioning Methods for Satisfiability Testing on Large Formulas.	CADE	1996	DBLP DOI BibTeX RDF
1	Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach	MUltlog 1.0: Towards an Expert System for Many-Valued Logics.	CADE	1996	DBLP DOI BibTeX RDF
1	Giuseppe De Giacomo, Fabio Massacci	Tableaux and Algorithms for Propositional Dynamic Logic with Converse.	CADE	1996	DBLP DOI BibTeX RDF
1	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
1	Harald Ganzinger, Uwe Waldmann	Theorem Proving in Cancellative Abelian Monoids (Extended Abstract).	CADE	1996	DBLP DOI BibTeX RDF
1	Claus Sengler	Termination of Algorithms over Non-freely Generated Data Types.	CADE	1996	DBLP DOI BibTeX RDF
1	Dongming Wang 0001	GEOTHER: A Geometry Theorem Prover.	CADE	1996	DBLP DOI BibTeX RDF
1	Steve Linton, Ursula Martin, Péter Pröhle, Duncan Shand	Algebra and Automated Deduction.	CADE	1996	DBLP DOI BibTeX RDF
1	Harald Ganzinger	Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract).	CADE	1996	DBLP DOI BibTeX RDF
1	Christian G. Fermüller	Semantic Trees Revisited: Some New Completeness Results.	CADE	1996	DBLP DOI BibTeX RDF
1	Miki Hermann, Phokion G. Kolaitis	Unification Algorithms Cannot be Combined in Polynomial Time.	CADE	1996	DBLP DOI BibTeX RDF
1	Andreas Nonnengart	Resolution-Based Calculi for Modal and Temporal Logics.	CADE	1996	DBLP DOI BibTeX RDF
1	Christoph Weidenbach	Unification in Pseudo-Linear Sort Theories is Decidable.	CADE	1996	DBLP DOI BibTeX RDF
1	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
1	Ursula Martin	Theorem Proving with Group Presentations: Examples and Questions.	CADE	1996	DBLP DOI BibTeX RDF
1	Deepak Kapur, Mahadevan Subramaniam	Lemma Discovery in Automated Induction.	CADE	1996	DBLP DOI BibTeX RDF
1	Harald Rueß	Reflection of Formal Tactics in a Deductive Reflection Framework.	CADE	1996	DBLP DOI BibTeX RDF
1	Jörg Denzinger, Stephan Schulz 0001	Learning Domain Knowledge to Improve Theorem Proving.	CADE	1996	DBLP DOI BibTeX RDF
1	Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann	The Tableau-based Theorem Prover 3TAP Version 4.0.	CADE	1996	DBLP DOI BibTeX RDF
1	Johann Schumann	SiCoTHEO: Simple Competitive Parallel Theorem Provers.	CADE	1996	DBLP DOI BibTeX RDF
1	Fausto Giunchiglia, Adolfo Villafiorita	ABSFOL: A Proof Checker with Abstraction.	CADE	1996	DBLP DOI BibTeX RDF
1	Clare Dixon	Search Strategies for Resolution in Temporal Logics.	CADE	1996	DBLP DOI BibTeX RDF
1	Eike Ritter, David J. Pym, Lincoln A. Wallen	Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract).	CADE	1996	DBLP DOI BibTeX RDF
1	Ole Rasmussen	An Embedding of Ruby in Isabelle.	CADE	1996	DBLP DOI BibTeX RDF
1	David A. McAllester, Kostas Arkoudas	Walther Recursion.	CADE	1996	DBLP DOI BibTeX RDF
1	Eric Domenjoud, Francis Klay, Christophe Ringeissen	Combination Techniques for Non-Disjoint Equational Theories.	CADE	1994	DBLP DOI BibTeX RDF
1	Penny Anderson	Representing Proof Transformations for Program Optimizations.	CADE	1994	DBLP DOI BibTeX RDF
1	Jian Zhang 0001	Problems on the Generation of Finite Models.	CADE	1994	DBLP DOI BibTeX RDF
1	John K. Slaney	The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure.	CADE	1994	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Xudong Zhao 0005	Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan.	CADE	1994	DBLP DOI BibTeX RDF
1	Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann	SETHEO V3.2: Recent Developments - System Abstract.	CADE	1994	DBLP DOI BibTeX RDF
1	Olav Lysne	On the Connection between Narrowing and Proof by Consistency.	CADE	1994	DBLP DOI BibTeX RDF
1	Peter Graf	Extended Path-Indexing.	CADE	1994	DBLP DOI BibTeX RDF
1	Bernhard Beckert	A Completion-Based Method for Mixed Universal and Rigid E-Unification.	CADE	1994	DBLP DOI BibTeX RDF
1	Frank Pfenning	Elf: A Meta-Language for Deductive Systems (System Descrition).	CADE	1994	DBLP DOI BibTeX RDF
1	Heng Chu, David A. Plaisted	Semantically Guided First-Order Theorem Proving using Hyper-Linking.	CADE	1994	DBLP DOI BibTeX RDF

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