default search action
13th CADE 1996: New Brunswick, NJ, USA
- Michael A. McRobbie, John K. Slaney:
Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings. Lecture Notes in Computer Science 1104, Springer 1996, ISBN 3-540-61511-3
Invited Lecture
- Harald Ganzinger:
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). 1
Session 1A
- Tanel Tammet:
A Resolution Theorem Prover for Intuitonistic Logic. 2-16 - Eike Ritter, David J. Pym, Lincoln A. Wallen:
Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). 17-31 - Andrei Voronkov:
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. 32-46
Session 1B
- Andrew Ireland, Alan Bundy:
Extensions to a Generalization Critic for Inductive Proof. 47-61 - Jörg Denzinger
, Stephan Schulz:
Learning Domain Knowledge to Improve Theorem Proving. 62-76 - Martin Protzen:
Patching Faulty Conjectures. 77-91
Session 2A
- Erica Melis, Jon Whittle:
Internal Analogy in Theorem Proving. 92-105 - Thomas Kolbe, Christoph Walther:
Termination of Theorem Proving by Reuse. 106-120 - Claus Sengler:
Termination of Algorithms over Non-freely Generated Data Types. 121-135
Session 2B
- Fausto Giunchiglia, Adolfo Villafiorita:
ABSFOL: A Proof Checker with Abstraction. 136-140 - Christoph Weidenbach, Bernd Gaede, Georg Rock:
SPASS & FLOTTER Version 0.42. 141-145 - Christian B. Suttner, Geoff Sutcliffe
The Design of the CADE-13 ATP System Competition. 146-160 - Hans Jürgen Ohlbach:
SCAN - Elimination of Predicate Quantifiers. 161-165 - Dongming Wang:
GEOTHER: A Geometry Theorem Prover. 166-170
Session 3A
- David A. Basin, Seán Matthews:
Structuring Metatheory on Inductive Definitions. 171-185 - Ole Rasmussen:
An Embedding of Ruby in Isabelle. 186-200 - Peter V. Homeier, David F. Martin:
Mechanical Verification of Mutually Recursive Procedures. 201-215
Session 3B
- Giovanni Felici, Giovanni Rinaldi, Klaus Truemper:
FasTraC: A Decentralized Traffic Control System Based on Logic Programming. 216-220 - Xiaorong Huang, Armin Fiedler:
Presenting Machine-Found Proofs. 221-225 - Matthias Baaz, Christian G. Fermüller, Gernot Salzer
MUltlog 1.0: Towards an Expert System for Many-Valued Logics. 226-230 - Janet Bertot, Yves Bertot:
CtCoq: A System Presentation. 231-234 - Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang:
An Introduction to Geometry Expert. 235-239 - Johann Schumann:
SiCoTHEO: Simple Competitive Parallel Theorem Provers. 240-244
Invited Lecture
- Dana S. Scott:
What Can We Hope to Achieve From Automated Deduction? (Abstract). 245
Session 4A
- Miki Hermann, Phokion G. Kolaitis:
Unification Algorithms Cannot be Combined in Polynomial Time. 246-260 - Qing Guo, Paliath Narendran, David A. Wolfram
Unification and Matching Modulo Nilpotence. 261-274 - Sergei G. Vorobyov:
An Improved Lower Bound for the Elementary Theories of Trees. 275-287
Session 4B
- Dieter Hutter, Claus Sengler:
INKA: The Next Generation. 288-292 - Torsten Schaub, Stefan Brüning, Pascal Nicolas:
XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description. 293-297 - William M. Farmer, Joshua D. Guttman
IMPS: An Updated System Description. 298-302 - Bernhard Beckert, Reiner Hähnle
The Tableau-based Theorem Prover 3TAP Version 4.0. 303-307 - Jian Zhang, Hantao Zhang:
System Description: Generating Models by SEM. 308-312
Session 5A
- John Harrison:
Optimizing Proof Search in Model Elimination. 313-327 - Konstantinos Sagonas
An Abstract Machine for Fixed-Order Dynamically Stratified Programs. 328-342 - Christoph Weidenbach:
Unification in Pseudo-Linear Sort Theories is Decidable. 343-357
Session 5B
- Ursula Martin
Theorem Proving with Group Presentations: Examples and Questions. 358-372 - Aart Middeldorp
Transforming Termination by Self-Labelling. 373-387 - Harald Ganzinger, Uwe Waldmann:
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). 388-402
Session 6A
- Uwe Egly, Thomas Rath:
On the Practical Value of Different Definitional Translations to Normal Form. 403-417 - Stephan Schmitt, Christoph Kreitz:
Converting Non-Classical Matrix Proofs into Sequent-Style Systems. 418-432 - Heribert Schütz, Tim Geisler:
Efficient Model Generation through Compilation. 433-447
Session 6B
- Steve Linton, Ursula Martin
Algebra and Automated Deduction. 448-462 - David Cyrluk, Patrick Lincoln, Natarajan Shankar:
On Shostak's Decision Procedure for Combinations of Theories. 463-477 - Thierry Boy de la Tour:
Ground Resolution with Group Computations on Semantic Symmetries. 478-492
Session 7A
- Olivier Roussel, Philippe Mathieu
A New Method for Knowledge Compilation: The Achievement by Cycle Search. 493-507 - Wayne Snyder, James G. Schmolze:
Rewrite Semantics for Production Rule Systems: Theory and Applications. 508-522 - Matthias Fuchs:
Experiments in the Heuristic Use of Past Proof Experience. 523-537
Session 7B
- Deepak Kapur, Mahadevan Subramaniam:
Lemma Discovery in Automated Induction. 538-552 - Peter Graf, Christoph Meyer:
Advanced Indexing Operations on Substitution Trees. 553-567 - Christian G. Fermüller:
Semantic Trees Revisited: Some New Completeness Results. 568-582
Session 8A
- Fausto Giunchiglia, Roberto Sebastiani:
Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. 583-597 - Andreas Nonnengart:
Resolution-Based Calculi for Modal and Temporal Logics. 598-612 - Giuseppe De Giacomo, Fabio Massacci
Tableaux and Algorithms for Propositional Dynamic Logic with Converse. 613-627
Session 8B
- Harald Rueß:
Reflection of Formal Tactics in a Deductive Reflection Framework. 628-642 - David A. McAllester, Kostas Arkoudas:
Walther Recursion. 643-657 - Amy P. Felty:
Proof Search with Set Variable Instantiation in the Calculus of Constructions. 658-672
Session 9A
- Clare Dixon
Search Strategies for Resolution in Temporal Logics. 673-687 - Gernot Salzer
Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. 688-702 - Saturnino F. Luz-Filho:
Grammar Specification in Categorial Logics and Theorem Proving. 703-717
Session 9B
- Peter Graf:
Path Indexing for AC-Theories. 718-732 - Tobias Nipkow
More Church-Rosser Proofs (in Isabelle/HOL). 733-747 - Tai Joon Park, Allen Van Gelder:
Partitioning Methods for Satisfiability Testing on Large Formulas. 748-762
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-22 19:50 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: