default search action
11th CADE 1992: Saratoga Springs, NY, USA
- Deepak Kapur:
Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings. Lecture Notes in Computer Science 607, Springer 1992, ISBN 3-540-55602-8
Session I: Keynote Address
- Larry Wos:
The Impossibility of the Automation of Logical Reasoning. 1-3
Session II
- Kurt Ammon:
Automatic Proofs in Mathematical Logic and Analysis. 4-19 - Shang-Ching Chou, Xiao-Shan Gao:
Proving Geometry Statements of Constructive Type. 20-34 - Larry M. Hines:
The Central Variable Strategy of Str+ve. 35-49
Session III A
- Franz Baader, Klaus U. Schulz:
Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. 50-65 - Tobias Nipkow, Zhenyu Qian:
Reduction and Unification in Lambda Calculi with Subtypes. 66-78 - Daniel J. Dougherty, Patricia Johann:
A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract). 79-93 - Wolfgang Bibel, Steffen Hölldobler, Jörg Würtz:
Cycle Unification. 94-108
Session III B
- Katherine A. Yelick
, Stephen J. Garland:
A Parallel Completion Procedure for Term Rewriting Systems. 109-123 - David A. McAllester:
Grammar Rewriting. 124-138 - Adam Cichon, Pierre Lescanne:
Polynomial Interpretations and the Complexity of Algorithms. 139-147 - Leonidas Fegaras, Tim Sheard, David W. Stemple:
Uniform Traversal Combinators: Definition, Use and Properties. 148-162
Session IV
- Tomás E. Uribe:
Sorted Unification Using Set Constraints. 163-177 - Alan M. Frisch
An Abstract View of Sorted Unification. 178-192 - Alexandre Boudet:
Unification in Order-Sorted Algebras with Overloading. 193-207
Session V: Banquet Address
- Raymond M. Smullyan:
Puzzles and Paradoxes (Abstract). 208
Session VI
- William McCune, Larry Wos:
Experiments in Automated Deduction with Condensed Detachment. 209-223 - Owen L. Astrachan, Mark E. Stickel:
Caching and Lemmaizing in Model Elimination Theorem Provers. 224-238 - Vincent J. Digricoli, Eugene Kochendorfer:
LIM+ Challenge Problems by RUE Hyper-Resolution. 239-252
Session VII
- Peter Jackson:
Computing Prime Implicates Incrementally. 253-267 - Geoff Sutcliffe
Linear-Input Subset Analysis. 268-280 - Belaid Benhamou, Lakhdar Sais:
Theoretical Study of Symmetries in Propositional Calculus and Applications. 281-294
Session VIII A
- David A. Basin, Toby Walsh:
Difference Matching. 295-309 - Jane Hesketh, Alan Bundy, Alan Smaill:
Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs. 310-324 - Toby Walsh, Alex Nunes, Alan Bundy:
The Use of Proof Plans to Sum Series. 325-339 - Martin Protzen:
Disproving Conjectures. 340-354
Session VIII B
- Mathias Bauer:
An Interval-based Temporal Logic in a Multivalued Setting. 355-369 - Michael Fisher:
A Normal Form for First-Order Temporal Formulae. 370-384 - Ricardo Caferra, Stéphane Demri:
Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic. 385-399 - Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa:
Embedding Negation as Failure into a Model Generation Theorem Prover. 400-415
Session IX
- Robert S. Boyer, Yuan Yu:
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. 416-430 - Hantao Zhang, Xin Hua:
Proving the Chinese Remainder Theorem by the Cover Set Induction. 431-445 - Peter Madden:
Automatic Program Optimization Through Proof Transformation. 446-460
Session X: Invited Talk
Session XI
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder:
Basic Paramodulation and Superposition. 462-476 - Robert Nieuwenhuis, Albert Rubio:
Theorem Proving with Ordering Constrained Clauses. 477-491 - Zohar Manna, Richard J. Waldinger:
The Special-Relation Rules are Incomplete. 492-506 - Bernhard Beckert, Reiner Hähnle:
An Improved Method for Adding Equality to Free Variable Semantic Tableaux. 507-521
Session XII A
- Natarajan Shankar:
Proof Search in the Intuitionistic Sequent Calculus. 522-536 - Frank Pfenning, Ekkehard Rohwedder:
Implementing the Meta-Theory of Deductive Systems. 537-551 - Wilfred Z. Chen:
Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic. 552-566 - William M. Farmer, Joshua D. Guttman
Little Theories. 567-581
Session XII B
- Jim Christian:
Some Termination Criteria for Narrowing and E-Narrowing. 582-588 - Nachum Dershowitz, Subrata Mitra, G. Sivakumar:
Decidable Matching for Convergent Systems (Preliminary Version). 589-602 - Delia Kesner:
Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors. 603-617 - R. C. Sekar, I. V. Ramakrishnan:
Programming with Equations: A Framework for Lazy Parallel Evaluation. 618-632
Session XIII
- Anthony G. Cohn:
A Many Sorted Logic with Possibly Empty Sorts. 633-647 - Andrei Voronkov:
Theorem Proving in Non-Standard Logics Based on the Inverse Method. 648-662 - Konstantin Vershinin, Igor Romanenko:
One More Logic with Uncertainty and Resolution Principle for it. 663-667
System Abstracts
- Li Dafa:
A Natural Deduction Automated Theorem Proving System. 668-672 - Tobias Nipkow, Lawrence C. Paulson
Isabelle-91. 673-676 - Geoff Sutcliffe
The Semantically Guided Linear Deduction System. 677-680 - Kurt Ammon:
The SHUNYATA System. 681-685 - Shang-Ching Chou:
A Geometry Theorem Prover for Macintoshes. 686-690 - Xin Hua, Hantao Zhang:
FRI: Failure-Resistant Induction in RRL. 691-695 - Hantao Zhang:
Herky: High Performance Rewriting in RRL. 696-700 - William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
IMPS: System Description. 701-705 - Geoffrey D. Alexander, David A. Plaisted:
Proving Equality Theorems with Hyper-Linking. 706-710 - Jawahar Chirimar, Carl A. Gunter, Myra Van Inwegen:
Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker. 711-715 - Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill:
&: Automated Natural Deduction. 716-720 - Tomás E. Uribe, Alan M. Frisch
An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems. 721-725 - Dave Barker-Plummer, Alex Rothenberg:
The GAZER Theorem Prover. 726-730 - Ewing L. Lusk, William McCune, John K. Slaney:
ROO: A Parallel Theorem Prover. 731-734 - Tie-Cheng Wang, Allen Goldberg:
RVF: An Automated Formal Verification System. 735-739 - Johann Schumann:
KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract). 740-742 - K. Blackburn:
A Report in ICL HOL. 743-747 - Sam Owre, John M. Rushby, Natarajan Shankar:
PVS: A Prototype Verification System. 748-752 - Wolfgang Reif:
The KIV System: Systematic Construction of Verified Software. 753-757 - Bernhard Beckert, Stefan Gerberding, Reiner Hähnle
The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics. 758-760 - Edmund M. Clarke, Xudong Zhao:
Analytica - A Theorem Prover in Mathematica. 761-765 - Klaus Schneider
The FAUST - Prover. 766-770 - Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, Mark Saaltink:
Eves System Description. 771-775 - Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita:
MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. 776-780
Problem Sets
- Ewing L. Lusk, Larry Wos:
Benchmark Problems in Which Equality Plays the Major Role. 781-785 - David A. Randell, Anthony G. Cohn, Zhan Cui:
Computing Transivity Tables: A Challenge For Automated Theorem Provers. 786-790
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-19 20:33 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: