Abstract is missing.
- The Impossibility of the Automation of Logical ReasoningLarry Wos. 1-3
- Automatic Proofs in Mathematical Logic and AnalysisKurt Ammon. 4-19
- Proving Geometry Statements of Constructive TypeShang-Ching Chou, Xiao-Shan Gao. 20-34
- The Central Variable Strategy of Str+veLarry M. Hines. 35-49
- Unification in the Union of Disjoint Equational Theories: Combining Decision ProceduresFranz Baader, Klaus U. Schulz. 50-65
- Reduction and Unification in Lambda Calculi with SubtypesTobias Nipkow, Zhenyu Qian. 66-78
- A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract)Daniel J. Dougherty, Patricia Johann. 79-93
- Cycle UnificationWolfgang Bibel, Steffen Hölldobler, Jörg Würtz. 94-108
- A Parallel Completion Procedure for Term Rewriting SystemsKatherine A. Yelick, Stephen J. Garland. 109-123
- Grammar RewritingDavid A. McAllester. 124-138
- Polynomial Interpretations and the Complexity of AlgorithmsAdam Cichon, Pierre Lescanne. 139-147
- Uniform Traversal Combinators: Definition, Use and PropertiesLeonidas Fegaras, Tim Sheard, David W. Stemple. 148-162
- Sorted Unification Using Set ConstraintsTomás E. Uribe. 163-177
- An Abstract View of Sorted UnificationAlan M. Frisch, Anthony G. Cohn. 178-192
- Unification in Order-Sorted Algebras with OverloadingAlexandre Boudet. 193-207
- Puzzles and Paradoxes (Abstract)Raymond M. Smullyan. 208
- Experiments in Automated Deduction with Condensed DetachmentWilliam McCune, Larry Wos. 209-223
- Caching and Lemmaizing in Model Elimination Theorem ProversOwen L. Astrachan, Mark E. Stickel. 224-238
- LIM+ Challenge Problems by RUE Hyper-ResolutionVincent J. Digricoli, Eugene Kochendorfer. 239-252
- Computing Prime Implicates IncrementallyPeter Jackson. 253-267
- Linear-Input Subset AnalysisGeoff Sutcliffe. 268-280
- Theoretical Study of Symmetries in Propositional Calculus and ApplicationsBelaid Benhamou, Lakhdar Sais. 281-294
- Difference MatchingDavid A. Basin, Toby Walsh. 295-309
- Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive ProgramsJane Hesketh, Alan Bundy, Alan Smaill. 310-324
- The Use of Proof Plans to Sum SeriesToby Walsh, Alex Nunes, Alan Bundy. 325-339
- Disproving ConjecturesMartin Protzen. 340-354
- An Interval-based Temporal Logic in a Multivalued SettingMathias Bauer. 355-369
- A Normal Form for First-Order Temporal FormulaeMichael Fisher. 370-384
- Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical LogicRicardo Caferra, Stéphane Demri. 385-399
- Embedding Negation as Failure into a Model Generation Theorem ProverKatsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa. 400-415
- Automated Correctness Proofs of Machine Code Programs for a Commercial MicroprocessorRobert S. Boyer, Yuan Yu. 416-430
- Proving the Chinese Remainder Theorem by the Cover Set InductionHantao Zhang, Xin Hua. 431-445
- Automatic Program Optimization Through Proof TransformationPeter Madden. 446-460
- Basic Paramodulation and SuperpositionLeo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder. 462-476
- Theorem Proving with Ordering Constrained ClausesRobert Nieuwenhuis, Albert Rubio. 477-491
- The Special-Relation Rules are IncompleteZohar Manna, Richard J. Waldinger. 492-506
- An Improved Method for Adding Equality to Free Variable Semantic TableauxBernhard Beckert, Reiner Hähnle. 507-521
- Proof Search in the Intuitionistic Sequent CalculusNatarajan Shankar. 522-536
- Implementing the Meta-Theory of Deductive SystemsFrank Pfenning, Ekkehard Rohwedder. 537-551
- Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and OnticWilfred Z. Chen. 552-566
- Little TheoriesWilliam M. Farmer, Joshua D. Guttman, F. Javier Thayer. 567-581
- Some Termination Criteria for Narrowing and E-NarrowingJim Christian. 582-588
- Decidable Matching for Convergent Systems (Preliminary Version)Nachum Dershowitz, Subrata Mitra, G. Sivakumar. 589-602
- Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with ConstructorsDelia Kesner. 603-617
- Programming with Equations: A Framework for Lazy Parallel EvaluationR. C. Sekar, I. V. Ramakrishnan. 618-632
- A Many Sorted Logic with Possibly Empty SortsAnthony G. Cohn. 633-647
- Theorem Proving in Non-Standard Logics Based on the Inverse MethodAndrei Voronkov. 648-662
- One More Logic with Uncertainty and Resolution Principle for itKonstantin Vershinin, Igor Romanenko. 663-667
- A Natural Deduction Automated Theorem Proving SystemLi Dafa. 668-672
- Isabelle-91Tobias Nipkow, Lawrence C. Paulson. 673-676
- The Semantically Guided Linear Deduction SystemGeoff Sutcliffe. 677-680
- The SHUNYATA SystemKurt Ammon. 681-685
- A Geometry Theorem Prover for MacintoshesShang-Ching Chou. 686-690
- FRI: Failure-Resistant Induction in RRLXin Hua, Hantao Zhang. 691-695
- Herky: High Performance Rewriting in RRLHantao Zhang. 696-700
- IMPS: System DescriptionWilliam M. Farmer, Joshua D. Guttman, F. Javier Thayer. 701-705
- Proving Equality Theorems with Hyper-LinkingGeoffrey D. Alexander, David A. Plaisted. 706-710
- Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof CheckerJawahar Chirimar, Carl A. Gunter, Myra Van Inwegen. 711-715
- &: Automated Natural DeductionDave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill. 716-720
- An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure SystemsTomás E. Uribe, Alan M. Frisch, Michael K. Mitchell. 721-725
- The GAZER Theorem ProverDave Barker-Plummer, Alex Rothenberg. 726-730
- ROO: A Parallel Theorem ProverEwing L. Lusk, William McCune, John K. Slaney. 731-734
- RVF: An Automated Formal Verification SystemTie-Cheng Wang, Allen Goldberg. 735-739
- KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract)Johann Schumann. 740-742
- A Report in ICL HOLK. Blackburn. 743-747
- PVS: A Prototype Verification SystemSam Owre, John M. Rushby, Natarajan Shankar. 748-752
- The KIV System: Systematic Construction of Verified SoftwareWolfgang Reif. 753-757
- The Tableau-Based Theorem Prover ::3::T:::A:::P for Multi-Valued LogicsBernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig. 758-760
- Analytica - A Theorem Prover in MathematicaEdmund M. Clarke, Xudong Zhao. 761-765
- The FAUST - ProverKlaus Schneider, Ramayya Kumar, Thomas Kropf. 766-770
- Eves System DescriptionDan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, Mark Saaltink. 771-775
- MGTP: A Parallel Theorem Prover Based on Lazy Model GenerationRyuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita. 776-780
- Benchmark Problems in Which Equality Plays the Major RoleEwing L. Lusk, Larry Wos. 781-785
- Computing Transivity Tables: A Challenge For Automated Theorem ProversDavid A. Randell, Anthony G. Cohn, Zhan Cui. 786-790