Larry Wos

J. Autom. Reason., 2017

2014

OTTER Proofs in Tarskian Geometry.

[BibT_eX]

[DOI]

Michael Beeson

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

The Legacy of a Great Researcher.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning and Mathematics, 2013

2006

Milestones for Automated Reasoning with Otter.

[BibT_eX]

[DOI]

Int. J. Artif. Intell. Tools, 2006

2005

Double-Negation Elimination in Some Propositional Logics.

[BibT_eX]

[DOI]

Michael Beeson

Robert Veroff

Stud Logica, 2005

The Flowering of Automated Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Mechanizing Mathematical Reasoning, 2005

2003

The Strategy of Cramming.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

2002

Shortest Axiomatizations of Implicational S4 and S5.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 2002

Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus.

[BibT_eX]

[DOI]

Dolph Ulrich

J. Autom. Reason., 2002

Hilbert's Twenty-Fourth Problem.

[BibT_eX]

[DOI]

Ruediger Thiele

J. Autom. Reason., 2002

Short Single Axioms for Boolean Algebra.

[BibT_eX]

[DOI]

J. Autom. Reason., 2002

XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus

[BibT_eX]

[DOI]

Dolph Ulrich

CoRR, 2002

Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus

[BibT_eX]

[DOI]

Dolph Ulrich

CoRR, 2002

A Spectrum of Applications of Automated Reasoning

[BibT_eX]

[DOI]

CoRR, 2002

2001

Finding Missing Proofs with Automated Reasoning.

[BibT_eX]

[DOI]

Stud Logica, 2001

Conquering the Meredith Single Axiom.

[BibT_eX]

[DOI]

J. Autom. Reason., 2001

A Milestone Reached and a Secret Revealed.

[BibT_eX]

[DOI]

J. Autom. Reason., 2001

Missing Proofs Found.

[BibT_eX]

[DOI]

J. Autom. Reason., 2001

2000

Automating the Search for Answers to Open Questions.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Appendix: Conjectures Concerning Proof, Design, and Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999

The Hot List Strategy.

[BibT_eX]

[DOI]

Gail W. Pieper

J. Autom. Reason., 1999

1998

Automating the Search for Elegant Proofs.

[BibT_eX]

[DOI]

J. Autom. Reason., 1998

Programs That Offer Fast, Flawless, Logical Reasoning.

[BibT_eX]

[DOI]

Commun. ACM, 1998

1997

Otter - The CADE-13 Competition Incarnations.

[BibT_eX]

[DOI]

J. Autom. Reason., 1997

1996

OTTER and the Moufang Identity Problem.

[BibT_eX]

[DOI]

J. Autom. Reason., 1996

The Power of Combining Resonance with Heat.

[BibT_eX]

[DOI]

J. Autom. Reason., 1996

1995

Searching for Circles of Pure Proofs.

[BibT_eX]

[DOI]

J. Autom. Reason., 1995

1994

The problem of hyperparamodulation.

[BibT_eX]

[DOI]

J. Autom. Reason., 1994

Logical basis for the automation of reasoning: Case studies.

[BibT_eX]

Robert Veroff

Proceedings of the Handbook of Logic in Artificial Intelligence and Logic Programming, 1994

1993

The Problem of Induction.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

The Problem of Reasoning by Case Analysis.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

The Problem of Naming and Function Replacement.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

The Problem of Reasoning by Analogy.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

The Kernel Strategy and Its Use for the Study of Combinatory Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

The Problem of Selecting an Approach Based on Prior Success.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

The Problem of Automated Theorem Finding.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

1992

The Problem of Demodulating Across Argument and Literal Boundaries.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

The Problem of Demodulator Adjunction.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

Note on McCune's Article on Discrimination Trees.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

The Problem of Demodulation During Inference Rule Application.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

The Problem of Reasoning from Inequalities.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

The Problem of Choosing between Using and Avoiding Eqyality Predicates.

[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

The Impossibility of the Automation of Logical Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

Experiments in Automated Deduction with Condensed Detachment.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

Benchmark Problems in Which Equality Plays the Major Role.

[BibT_eX]

[DOI]

Ewing L. Lusk

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

The Problem of Choosing the Representation, Inference Rule, and Strategy.

[BibT_eX]

[DOI]

J. Autom. Reason., 1991

The Problem of Choosing the Type of Subsumption to Use.

[BibT_eX]

[DOI]

J. Autom. Reason., 1991

The Problem of Finding a Restriction Strategy More Effective Than the Set of Support Strategy.

[BibT_eX]

[DOI]

J. Autom. Reason., 1991

Subsumption, a Sometimes Undervalued Procedure.

[BibT_eX]

Ewing L. Lusk

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

Automated Reasoning and Bledsoe's Dream for the Field.

[BibT_eX]

Proceedings of the Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991

1990

The Problem of Choosing between Predicate and Function Notation for Problem Representation.

[BibT_eX]

[DOI]

J. Autom. Reason., 1990

The Problem of Finding a Semantic Strategy for Focusing Inference Rules.

[BibT_eX]

[DOI]

J. Autom. Reason., 1990

Meeting the Challenge of Fifty Years of Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 1990

The Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation.

[BibT_eX]

[DOI]

J. Autom. Reason., 1990

The Problem of Choosing between Logic Programming and General-Purpose Automated Reasoning.

[BibT_eX]

[DOI]

J. Autom. Reason., 1990

Automated Reasoning Contributed to Mathematics and Logic.

[BibT_eX]

[DOI]

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

1989

The Problem of Guaranteeing the Absence of a Complete Set of Reductions.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

The Problem of Guaranteeing the Existence of a Complete Set of Reductions.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

The Problem of Determining the Size of a Complete Set of Reductions.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

The Problem of Finding an Inference Rule for Set Theory.

[BibT_eX]

[DOI]

J. Autom. Reason., 1989

1988

The Problem of Self-Analytically Choosing the Weights.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

The Problem of Self-Analytically Choosing the Set of Support.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

The Problem of Finding a Strategy to Control Binary Paramodulation.

[BibT_eX]

[DOI]

J. Autom. Reason., 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

Automated reasoning - 33 basic research problems.

[BibT_eX]

Prentice Hall, ISBN: 978-0-13-054552-7, 1988

1987

The Problem of Definition Expansion and Contraction.

[BibT_eX]

[DOI]

J. Autom. Reason., 1987

The Problem of Extending the Set of Support Strategy.

[BibT_eX]

[DOI]

J. Autom. Reason., 1987

The Problem of Choosing the Inference Rule to Employ.

[BibT_eX]

[DOI]

J. Autom. Reason., 1987

Some Obstacles to the Automation of Reasoning and the Problem of Redundant Information.

[BibT_eX]

[DOI]

J. Autom. Reason., 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

Negative Paramodulation.

[BibT_eX]

[DOI]

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

1985

What Is Automated Reasoning?

[BibT_eX]

J. Autom. Reason., 1985

Editorial: A Journal Is Born.

[BibT_eX]

[DOI]

J. Autom. Reason., 1985

1984

A New Use of an Automated Reasoning Assistant: Open Questions in Equivalential Calculus and the Study of Infinite Domains.

[BibT_eX]

[DOI]

Artif. Intell., 1984

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

[BibT_eX]

[DOI]

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

1983

Questions concerning possible shortest single axioms for the equivalential calculus: an application of automated theorem proving to infinite domains.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 1983

Automated Reasoning: Real Uses and Potential Uses.

[BibT_eX]

[DOI]

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

1982

Solving Open Questions with an Automated Theorem-Proving Program.

[BibT_eX]

[DOI]

Proceedings of the 6th Conference on Automated Deduction, 1982

Procedure Implementation Through Demodulation and Related Tricks.

[BibT_eX]

[DOI]

Steven K. Winker

Proceedings of the 6th Conference on Automated Deduction, 1982

1981

An automated reasoning system.

[BibT_eX]

[DOI]

Steven K. Winker

Ewing L. Lusk

Proceedings of the American Federation of Information Processing Societies: 1981 National Computer Conference, 1981

1980

Hyperparamodulation: A Refinement of Paramodulation.

[BibT_eX]

[DOI]

Lawrence J. Henschen

Proceedings of the 5th Conference on Automated Deduction, 1980

1978

Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra.

[BibT_eX]

[DOI]

Steve Winker

Proceedings of the eighth international symposium on Multiple-valued logic, 1978

1976

Problems and Experiments for and with Automated Theorem-Proving Programs.

[BibT_eX]

[DOI]

John D. McCharen

IEEE Trans. Computers, 1976

1974

Unit Refutations and Horn Sets.

[BibT_eX]

[DOI]

Lawrence J. Henschen

J. ACM, 1974

A Theorem-Proving Language for Experimentation.

[BibT_eX]

[DOI]

Lawrence J. Henschen

Commun. ACM, 1974

1967

The Concept of Demodulation in Theorem Proving.

[BibT_eX]

[DOI]

J. ACM, 1967

1965

Efficiency and Completeness of the Set of Support Strategy in Theorem Proving.

[BibT_eX]

[DOI]

George A. Robinson

Daniel F. Carson

J. ACM, 1965

1964

The unit preference strategy in theorem proving.

[BibT_eX]

[DOI]