William McCune

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

Semantic Guidance for Saturation Provers.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 2006

2004

Encapsulation for Practical Simplification Procedures

[BibT_eX]

[DOI]

Olga Shumsky Matlin

CoRR, 2004

2003

OTTER 3.3 Reference Manual

[BibT_eX]

[DOI]

CoRR, 2003

Mace4 Reference Manual and Guide

[BibT_eX]

[DOI]

CoRR, 2003

Methods to Model-Check Parallel Systems Software

[BibT_eX]

[DOI]

Olga Shumsky Matlin

CoRR, 2003

2002

Short Single Axioms for Boolean Algebra.

[BibT_eX]

[DOI]

J. Autom. Reason., 2002

SPINning Parallel Systems Software.

[BibT_eX]

[DOI]

Olga Shumsky Matlin

Proceedings of the Model Checking of Software, 2002

2001

MACE 2.0 Reference Manual and Guide

[BibT_eX]

[DOI]

CoRR, 2001

2000

System Description: IVY.

[BibT_eX]

[DOI]

Olga Shumsky

Proceedings of the Automated Deduction, 2000

1998

Automatic Proofs and Counterexamples for Some Ortholattice Identities.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1998

1997

Otter - The CADE-13 Competition Incarnations.

[BibT_eX]

[DOI]

J. Autom. Reason., 1997

Solution of the Robbins Problem.

[BibT_eX]

[DOI]

J. Autom. Reason., 1997

Direct finite first-order model generation with negative constraint propagation heuristic.

[BibT_eX]

[DOI]

Proceedings of the 1997 ACM symposium on Applied Computing, 1997

Well-Behaved Search and the Robbins Problem.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

1996

Automated Deduction in Equational Logic and Cubic Curves

[BibT_eX]

[DOI]

R. Padmanabhan

Lecture Notes in Computer Science 1095, Springer, ISBN: 3-540-61398-6, 1996

1994

SCOTT: Semantically Constrained Otter System Description.

[BibT_eX]

[DOI]

John K. Slaney

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Distributed Theorem Proving by Peers.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

Single Axioms for the Left Group and the Right Group Calculi.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 1993

Single Axioms for Groups and Abelian Groups with Various Operations.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

Uniform Strategies: The CADE-11 Theorem Proving Contest.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

1992

Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

The Application of Automated Reasoning to Questions in Mathematics and Logic.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 1992

Application of Automated Deduction to the Search for Single Axioms for Exponent Groups.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Automated Reasoning, 1992

Experiments in Automated Deduction with Condensed Detachment.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

ROO: A Parallel Theorem Prover.

[BibT_eX]

[DOI]

John K. Slaney

Proceedings of the Automated Deduction, 1992

1991

The Absence and the Presence of Fixed Point Combinators.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1991

Automated Theorem Proving and Logic Programming.

[BibT_eX]

[DOI]

J. Log. Program., 1991

1990

Parallel Closure-Based Automated Reasoning.

[BibT_eX]

John K. Slaney

Proceedings of the Parallelization in Inference Systems, 1990

Experiments with ROO: A Parallel Automated Deduction System.

[BibT_eX]

[DOI]

Proceedings of the Parallelization in Inference Systems, 1990

Automated Reasoning Contributed to Mathematics and Logic.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Automated Deduction, 1990

OTTER 2.0.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Automated Deduction, 1990

Tutorial on High-Performance Automated Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Automated Deduction, 1990

Skolem Functions and Equality in Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the 8th National Conference on Artificial Intelligence. Boston, Massachusetts, USA, July 29, 1990

1989

Automated Reasoning about Elementary Point-Set Topology.

[BibT_eX]

[DOI]

Cynthia A. Wick

J. Autom. Reason., 1989

Maintaining state constraints in relational databases: a proof theoretic basis.

[BibT_eX]

[DOI]

J. ACM, 1989

1988

Un-Skolemizing Clause Sets.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1988

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

Challenge Equality Problems in Lattice Theory.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 1987

1986

Set Theory in First-Order Logic: Clauses for Gödel's Axioms.

[BibT_eX]

[DOI]

J. Autom. Reason., 1986

Parallel Logic Programming for Numeric Applications.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on Logic Programming, 1986

Negative Paramodulation.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

ITP at Argonne National Laboratory.

[BibT_eX]

[DOI]

Ross A. Overbeek

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Paths to High-Performance Automated Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

Experiments with Semantic Paramodulation.

[BibT_eX]

[DOI]

J. Autom. Reason., 1985

1984

The Linked Inference Principle, II: The User's Viewpoint.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Automated Deduction, 1984

1983

Semantic Paramodulation for Horn Sets.

[BibT_eX]

[DOI]

Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

1982

Logic Machine Architecture: Inference Mechanisms.

[BibT_eX]

[DOI]

Ross A. Overbeek

Proceedings of the 6th Conference on Automated Deduction, 1982

Logic Machine Architecture: Kernel Funtions.

[BibT_eX]

[DOI]

Ross A. Overbeek

Proceedings of the 6th Conference on Automated Deduction, 1982

Compiling Constraint-Checking Programs from First-Order Formulas.

[BibT_eX]