The unit preference strategy in theorem proving. - Larry Wos; Daniel F. Carson; George A. Robinson (AFIPS Fall Joint Computing Conference (1), 1964)

Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. - Larry Wos; George A. Robinson; Daniel F. Carson (J. ACM, 1965)

The Concept of Demodulation in Theorem Proving. - Larry Wos; George A. Robinson; Daniel F. Carson; Leon Shalla (J. ACM, 1967)

A Theorem-Proving Language for Experimentation. - Lawrence J. Henschen; Ross A. Overbeek; Larry Wos (Commun. ACM, 1974)

Unit Refutations and Horn Sets. - Lawrence J. Henschen; Larry Wos (J. ACM, 1974)

Problems and Experiments for and with Automated Theorem-Proving Programs. - John D. McCharen; Ross A. Overbeek; Larry Wos (IEEE Trans. Computers, 1976)

Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra. - Steve Winker; Larry Wos (MVL, 1978)

Hyperparamodulation: A Refinement of Paramodulation. - Larry Wos; Ross A. Overbeek; Lawrence J. Henschen (CADE, 1980)

An automated reasoning system. - Larry Wos; Steven K. Winker; Ewing L. Lusk (AFIPS National Computer Conference, 1981)

Procedure Implementation Through Demodulation and Related Tricks. - Steven K. Winker; Larry Wos (CADE, 1982)

Solving Open Questions with an Automated Theorem-Proving Program. - Larry Wos (CADE, 1982)

Automated Reasoning: Real Uses and Potential Uses. - Larry Wos (IJCAI, 1983)

Questions concerning possible shortest single axioms for the equivalential calculus: an application of automated theorem proving to infinite domains. - Larry Henschen; Barry Smith 002; Robert Veroff; Steve Winker; Larry Wos (Notre Dame J. Formal Log., 1983)

The Linked Inference Principle, II: The User's Viewpoint. - Larry Wos; Robert Veroff; Barry Smith 002; William McCune (CADE, 1984)

A New Use of an Automated Reasoning Assistant: Open Questions in Equivalential Calculus and the Study of Infinite Domains. - Larry Wos; Steve Winker; Barry Smith 002; Robert Veroff; Lawrence J. Henschen (Artif. Intell., 1984)

Editorial: A Journal Is Born. - Larry Wos (J. Autom. Reason., 1985)

What Is Automated Reasoning? - Larry Wos (J. Autom. Reason., 1985)

Negative Paramodulation. - Larry Wos; William McCune (CADE, 1986)

Set Theory in First-Order Logic: Clauses for Gödel's Axioms. - Robert S. Boyer; Ewing L. Lusk; William McCune; Ross A. Overbeek; Mark E. Stickel; Larry Wos (J. Autom. Reason., 1986)

A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. - William McCune; Larry Wos (J. Autom. Reason., 1987)

Some Obstacles to the Automation of Reasoning and the Problem of Redundant Information. - Larry Wos (J. Autom. Reason., 1987)

The Problem of Choosing the Inference Rule to Employ. - Larry Wos (J. Autom. Reason., 1987)

The Problem of Extending the Set of Support Strategy. - Larry Wos (J. Autom. Reason., 1987)

The Problem of Definition Expansion and Contraction. - Larry Wos (J. Autom. Reason., 1987)

Automated reasoning - 33 basic research problems. - Larry Wos (Prentice Hall, 1988)

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. - Larry Wos; William McCune (CADE, 1988)

The Problem of Finding a Strategy to Control Binary Paramodulation. - Larry Wos (J. Autom. Reason., 1988)

The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation. - Larry Wos (J. Autom. Reason., 1988)

The Problem of Self-Analytically Choosing the Set of Support. - Larry Wos (J. Autom. Reason., 1988)

The Problem of Self-Analytically Choosing the Weights. - Larry Wos (J. Autom. Reason., 1988)

The Problem of Finding an Inference Rule for Set Theory. - Larry Wos (J. Autom. Reason., 1989)

The Problem of Determining the Size of a Complete Set of Reductions. - Larry Wos (J. Autom. Reason., 1989)

The Problem of Guaranteeing the Existence of a Complete Set of Reductions. - Larry Wos (J. Autom. Reason., 1989)

The Problem of Guaranteeing the Absence of a Complete Set of Reductions. - Larry Wos (J. Autom. Reason., 1989)

Automated Reasoning Contributed to Mathematics and Logic. - Larry Wos; Steve Winker; William McCune; Ross A. Overbeek; Ewing L. Lusk; Rick L. Stevens; Ralph Butler (CADE, 1990)

The Problem of Choosing between Logic Programming and General-Purpose Automated Reasoning. - Larry Wos (J. Autom. Reason., 1990)

The Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation. - Larry Wos (J. Autom. Reason., 1990)

Meeting the Challenge of Fifty Years of Logic. - Larry Wos (J. Autom. Reason., 1990)

The Problem of Finding a Semantic Strategy for Focusing Inference Rules. - Larry Wos (J. Autom. Reason., 1990)

The Problem of Choosing between Predicate and Function Notation for Problem Representation. - Larry Wos (J. Autom. Reason., 1990)

Automated Reasoning and Bledsoe's Dream for the Field. - Larry Wos (Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991)

Subsumption, a Sometimes Undervalued Procedure. - Larry Wos; Ross A. Overbeek; Ewing L. Lusk (Computational Logic - Essays in Honor of Alan Robinson, 1991)

The Problem of Finding a Restriction Strategy More Effective Than the Set of Support Strategy. - Larry Wos (J. Autom. Reason., 1991)

The Problem of Choosing the Type of Subsumption to Use. - Larry Wos (J. Autom. Reason., 1991)

The Problem of Choosing the Representation, Inference Rule, and Strategy. - Larry Wos (J. Autom. Reason., 1991)

Automated Theorem Proving and Logic Programming. - Larry Wos; William McCune (J. Log. Program., 1991)

The Absence and the Presence of Fixed Point Combinators. - William McCune; Larry Wos (Theor. Comput. Sci., 1991)

Benchmark Problems in Which Equality Plays the Major Role. - Ewing L. Lusk; Larry Wos (CADE, 1992)

Experiments in Automated Deduction with Condensed Detachment. - William McCune; Larry Wos (CADE, 1992)

The Impossibility of the Automation of Logical Reasoning. - Larry Wos (CADE, 1992)

Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. - William McCune; Larry Wos (LPAR, 1992)

The Application of Automated Reasoning to Questions in Mathematics and Logic. - Larry Wos; William McCune (Ann. Math. Artif. Intell., 1992)

The Problem of Choosing between Using and Avoiding Eqyality Predicates. - Larry Wos (J. Autom. Reason., 1992)

The Problem of Reasoning from Inequalities. - Larry Wos (J. Autom. Reason., 1992)

The Problem of Demodulation During Inference Rule Application. - Larry Wos (J. Autom. Reason., 1992)

Note on McCune's Article on Discrimination Trees. - Larry Wos (J. Autom. Reason., 1992)

The Problem of Demodulator Adjunction. - Larry Wos (J. Autom. Reason., 1992)

The Problem of Demodulating Across Argument and Literal Boundaries. - Larry Wos (J. Autom. Reason., 1992)

The Problem of Automated Theorem Finding. - Larry Wos (J. Autom. Reason., 1993)

The Problem of Selecting an Approach Based on Prior Success. - Larry Wos (J. Autom. Reason., 1993)

The Kernel Strategy and Its Use for the Study of Combinatory Logic. - Larry Wos (J. Autom. Reason., 1993)

The Problem of Reasoning by Analogy. - Larry Wos (J. Autom. Reason., 1993)

The Problem of Naming and Function Replacement. - Larry Wos (J. Autom. Reason., 1993)

The Problem of Reasoning by Case Analysis. - Larry Wos (J. Autom. Reason., 1993)

The Problem of Induction. - Larry Wos (J. Autom. Reason., 1993)

Logical basis for the automation of reasoning: Case studies. - Larry Wos; Robert Veroff (Handbook of Logic in Artificial Intelligence and Logic Programming (2), 1994)

The problem of hyperparamodulation. - Larry Wos (J. Autom. Reason., 1994)

Searching for Circles of Pure Proofs. - Larry Wos (J. Autom. Reason., 1995)

The Power of Combining Resonance with Heat. - Larry Wos (J. Autom. Reason., 1996)

OTTER and the Moufang Identity Problem. - Larry Wos (J. Autom. Reason., 1996)

Otter - The CADE-13 Competition Incarnations. - William McCune; Larry Wos (J. Autom. Reason., 1997)

Programs That Offer Fast, Flawless, Logical Reasoning. - Larry Wos (Commun. ACM, 1998)

Automating the Search for Elegant Proofs. - Larry Wos (J. Autom. Reason., 1998)

The Hot List Strategy. - Larry Wos; Gail W. Pieper (J. Autom. Reason., 1999)

Appendix: Conjectures Concerning Proof, Design, and Verification. - Larry Wos (TPHOLs, 2000)

Automating the Search for Answers to Open Questions. - Larry Wos; Branden Fitelson (TPHOLs, 2000)

Missing Proofs Found. - Branden Fitelson; Larry Wos (J. Autom. Reason., 2001)

A Milestone Reached and a Secret Revealed. - Larry Wos (J. Autom. Reason., 2001)

Conquering the Meredith Single Axiom. - Larry Wos (J. Autom. Reason., 2001)

Finding Missing Proofs with Automated Reasoning. - Branden Fitelson; Larry Wos (Stud Logica, 2001)

A Spectrum of Applications of Automated Reasoning - Larry Wos (CoRR, 2002)

Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus - Larry Wos; Dolph Ulrich; Branden Fitelson (CoRR, 2002)

XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus - Larry Wos; Dolph Ulrich; Branden Fitelson (CoRR, 2002)

Short Single Axioms for Boolean Algebra. - William McCune; Robert Veroff; Branden Fitelson; Kenneth Harris; Andrew Feist; Larry Wos (J. Autom. Reason., 2002)

Hilbert's Twenty-Fourth Problem. - Ruediger Thiele; Larry Wos (J. Autom. Reason., 2002)

Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus. - Larry Wos; Dolph Ulrich; Branden Fitelson (J. Autom. Reason., 2002)

Shortest Axiomatizations of Implicational S4 and S5. - Zachary Ernst; Branden Fitelson; Kenneth Harris; Larry Wos (Notre Dame J. Formal Log., 2002)

The Strategy of Cramming. - Larry Wos (J. Autom. Reason., 2003)

The Flowering of Automated Reasoning. - Larry Wos (Mechanizing Mathematical Reasoning, 2005)

Double-Negation Elimination in Some Propositional Logics. - Michael Beeson; Robert Veroff; Larry Wos (Stud Logica, 2005)

Milestones for Automated Reasoning with Otter. - Larry Wos (Int. J. Artif. Intell. Tools, 2006)

The Legacy of a Great Researcher. - Larry Wos (Automated Reasoning and Mathematics, 2013)

OTTER Proofs in Tarskian Geometry. - Michael Beeson; Larry Wos (IJCAR, 2014)

Finding Proofs in Tarskian Geometry. - Michael Beeson; Larry Wos (J. Autom. Reason., 2017)