default search action
Larry Wos
Person information
- affiliation: Argonne National Laboratory, Lemont, Illinois, USA
- award (1992): Herbrand Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2017
- [j67]Michael Beeson
, Larry Wos:
Finding Proofs in Tarskian Geometry. J. Autom. Reason. 58(1): 181-207 (2017) - 2016
- [i5]Michael Beeson, Larry Wos:
Finding Proofs in Tarskian Geometry. CoRR abs/1606.07095 (2016) - 2014
- [c22]Michael Beeson, Larry Wos:
OTTER Proofs in Tarskian Geometry. IJCAR 2014: 495-510 - 2013
- [c21]Larry Wos:
The Legacy of a Great Researcher. Automated Reasoning and Mathematics 2013: 1-14
2000 – 2009
- 2006
- [j66]Larry Wos:
Milestones for Automated Reasoning with Otter. Int. J. Artif. Intell. Tools 15(1): 3-20 (2006) - 2005
- [j65]Michael Beeson, Robert Veroff, Larry Wos:
Double-Negation Elimination in Some Propositional Logics. Stud Logica 80(2-3): 195-234 (2005) - [c20]Larry Wos:
The Flowering of Automated Reasoning. Mechanizing Mathematical Reasoning 2005: 204-227 - 2003
- [j64]Larry Wos:
The Strategy of Cramming. J. Autom. Reason. 30(2): 179-204 (2003) - [i4]Michael Beeson, Robert Veroff, Larry Wos:
Double-Negation Elimination in Some Propositional Logics. CoRR cs.LO/0301026 (2003) - 2002
- [j63]William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos:
Short Single Axioms for Boolean Algebra. J. Autom. Reason. 29(1): 1-16 (2002) - [j62]Ruediger Thiele, Larry Wos:
Hilbert's Twenty-Fourth Problem. J. Autom. Reason. 29(1): 67-89 (2002) - [j61]Larry Wos, Dolph Ulrich, Branden Fitelson:
Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus. J. Autom. Reason. 29(2): 107-124 (2002) - [j60]Zachary Ernst, Branden Fitelson, Kenneth Harris, Larry Wos:
Shortest Axiomatizations of Implicational S4 and S5. Notre Dame J. Formal Log. 43(3): 169-179 (2002) - [i3]Larry Wos:
A Spectrum of Applications of Automated Reasoning. CoRR cs.AI/0205078 (2002) - [i2]Larry Wos, Dolph Ulrich, Branden Fitelson:
Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus. CoRR cs.LO/0211014 (2002) - [i1]Larry Wos, Dolph Ulrich, Branden Fitelson:
XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus. CoRR cs.LO/0211015 (2002) - 2001
- [j59]Larry Wos:
A Milestone Reached and a Secret Revealed. J. Autom. Reason. 27(2): 89-95 (2001) - [j58]Larry Wos:
Conquering the Meredith Single Axiom. J. Autom. Reason. 27(2): 175-199 (2001) - [j57]Branden Fitelson, Larry Wos:
Missing Proofs Found. J. Autom. Reason. 27(2): 201-225 (2001) - [j56]Branden Fitelson, Larry Wos:
Finding Missing Proofs with Automated Reasoning. Stud Logica 68(3): 329-356 (2001) - 2000
- [c19]Larry Wos, Branden Fitelson:
Automating the Search for Answers to Open Questions. TPHOLs 2000: 519-525 - [c18]Larry Wos:
Appendix: Conjectures Concerning Proof, Design, and Verification. TPHOLs 2000: 526-533
1990 – 1999
- 1999
- [j55]Larry Wos, Gail W. Pieper:
The Hot List Strategy. J. Autom. Reason. 22(1): 1-44 (1999) - 1998
- [j54]Larry Wos:
Programs That Offer Fast, Flawless, Logical Reasoning. Commun. ACM 41(6): 87-95 (1998) - [j53]Larry Wos:
Automating the Search for Elegant Proofs. J. Autom. Reason. 21(2): 135-175 (1998) - 1997
- [j52]William McCune, Larry Wos:
Otter - The CADE-13 Competition Incarnations. J. Autom. Reason. 18(2): 211-220 (1997) - 1996
- [j51]Larry Wos:
The Power of Combining Resonance with Heat. J. Autom. Reason. 17(1): 23-81 (1996) - [j50]Larry Wos:
OTTER and the Moufang Identity Problem. J. Autom. Reason. 17(2): 215-257 (1996) - 1995
- [j49]Larry Wos:
Searching for Circles of Pure Proofs. J. Autom. Reason. 15(3): 279-315 (1995) - 1994
- [j48]Larry Wos:
The problem of hyperparamodulation. J. Autom. Reason. 12(2): 265-271 (1994) - [p1]Larry Wos, Robert Veroff:
Logical basis for the automation of reasoning: Case studies. Handbook of Logic in Artificial Intelligence and Logic Programming (2) 1994: 1-40 - 1993
- [j47]Larry Wos:
The Problem of Automated Theorem Finding. J. Autom. Reason. 10(1): 137-138 (1993) - [j46]Larry Wos:
The Problem of Selecting an Approach Based on Prior Success. J. Autom. Reason. 10(2): 283-284 (1993) - [j45]Larry Wos:
The Kernel Strategy and Its Use for the Study of Combinatory Logic. J. Autom. Reason. 10(3): 287-343 (1993) - [j44]Larry Wos:
The Problem of Reasoning by Analogy. J. Autom. Reason. 10(3): 421-422 (1993) - [j43]Larry Wos:
The Problem of Naming and Function Replacement. J. Autom. Reason. 11(1): 147-148 (1993) - [j42]Larry Wos:
The Problem of Reasoning by Case Analysis. J. Autom. Reason. 11(2): 289-291 (1993) - [j41]Larry Wos:
The Problem of Induction. J. Autom. Reason. 11(3): 433-434 (1993) - 1992
- [j40]Larry Wos, William McCune:
The Application of Automated Reasoning to Questions in Mathematics and Logic. Ann. Math. Artif. Intell. 5(2-4): 321-369 (1992) - [j39]Larry Wos:
The Problem of Choosing between Using and Avoiding Eqyality Predicates. J. Autom. Reason. 8(2): 307-309 (1992) - [j38]Larry Wos:
The Problem of Reasoning from Inequalities. J. Autom. Reason. 8(3): 421-426 (1992) - [j37]Larry Wos:
The Problem of Demodulation During Inference Rule Application. J. Autom. Reason. 9(1): 141-143 (1992) - [j36]Larry Wos:
Note on McCune's Article on Discrimination Trees. J. Autom. Reason. 9(2): 145-146 (1992) - [j35]Larry Wos:
The Problem of Demodulator Adjunction. J. Autom. Reason. 9(2): 289-290 (1992) - [j34]Larry Wos:
The Problem of Demodulating Across Argument and Literal Boundaries. J. Autom. Reason. 9(3): 407-408 (1992) - [c17]Larry Wos:
The Impossibility of the Automation of Logical Reasoning. CADE 1992: 1-3 - [c16]William McCune, Larry Wos:
Experiments in Automated Deduction with Condensed Detachment. CADE 1992: 209-223 - [c15]Ewing L. Lusk, Larry Wos:
Benchmark Problems in Which Equality Plays the Major Role. CADE 1992: 781-785 - [c14]William McCune, Larry Wos:
Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. LPAR 1992: 131-136 - 1991
- [j33]Larry Wos:
The Problem of Finding a Restriction Strategy More Effective Than the Set of Support Strategy. J. Autom. Reason. 7(1): 105-107 (1991) - [j32]Larry Wos:
The Problem of Choosing the Type of Subsumption to Use. J. Autom. Reason. 7(3): 435-438 (1991) - [j31]Larry Wos:
The Problem of Choosing the Representation, Inference Rule, and Strategy. J. Autom. Reason. 7(4): 631-634 (1991) - [j30]Larry Wos, William McCune:
Automated Theorem Proving and Logic Programming. J. Log. Program. 11(1&2): 1-53 (1991) - [j29]William McCune, Larry Wos:
The Absence and the Presence of Fixed Point Combinators. Theor. Comput. Sci. 87(1): 221-228 (1991) - [c13]Larry Wos, Ross A. Overbeek, Ewing L. Lusk:
Subsumption, a Sometimes Undervalued Procedure. Computational Logic - Essays in Honor of Alan Robinson 1991: 3-40 - [c12]Larry Wos:
Automated Reasoning and Bledsoe's Dream for the Field. Automated Reasoning: Essays in Honor of Woody Bledsoe 1991: 297-345 - 1990
- [j28]Larry Wos:
The Problem of Choosing between Logic Programming and General-Purpose Automated Reasoning. J. Autom. Reason. 6(1): 77-78 (1990) - [j27]Larry Wos:
The Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation. J. Autom. Reason. 6(2): 211-212 (1990) - [j26]Larry Wos:
Meeting the Challenge of Fifty Years of Logic. J. Autom. Reason. 6(2): 213-232 (1990) - [j25]Larry Wos:
The Problem of Finding a Semantic Strategy for Focusing Inference Rules. J. Autom. Reason. 6(3): 337-339 (1990) - [j24]Larry Wos:
The Problem of Choosing between Predicate and Function Notation for Problem Representation. J. Autom. Reason. 6(4): 463-464 (1990) - [c11]Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler:
Automated Reasoning Contributed to Mathematics and Logic. CADE 1990: 485-499
1980 – 1989
- 1989
- [j23]Larry Wos:
The Problem of Finding an Inference Rule for Set Theory. J. Autom. Reason. 5(1): 93-95 (1989) - [j22]Larry Wos:
The Problem of Determining the Size of a Complete Set of Reductions. J. Autom. Reason. 5(2): 235-237 (1989) - [j21]Larry Wos:
The Problem of Guaranteeing the Existence of a Complete Set of Reductions. J. Autom. Reason. 5(3): 399-401 (1989) - [j20]Larry Wos:
The Problem of Guaranteeing the Absence of a Complete Set of Reductions. J. Autom. Reason. 5(4): 531-532 (1989) - 1988
- [b1]Larry Wos:
Automated reasoning - 33 basic research problems. Prentice Hall 1988, ISBN 978-0-13-054552-7, pp. I-XIII, 1-319 - [j19]Larry Wos:
The Problem of Finding a Strategy to Control Binary Paramodulation. J. Autom. Reason. 4(1): 101-107 (1988) - [j18]Larry Wos:
The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation. J. Autom. Reason. 4(2): 215-217 (1988) - [j17]Larry Wos:
The Problem of Self-Analytically Choosing the Set of Support. J. Autom. Reason. 4(3): 327-329 (1988) - [j16]Larry Wos:
The Problem of Self-Analytically Choosing the Weights. J. Autom. Reason. 4(4): 463-464 (1988) - [c10]Larry Wos, William McCune:
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. CADE 1988: 714-729 - 1987
- [j15]Larry Wos:
Some Obstacles to the Automation of Reasoning and the Problem of Redundant Information. J. Autom. Reason. 3(1): 81-90 (1987) - [j14]William McCune, Larry Wos:
A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. J. Autom. Reason. 3(1): 91-107 (1987) - [j13]Larry Wos:
The Problem of Choosing the Inference Rule to Employ. J. Autom. Reason. 3(2): 201-209 (1987) - [j12]Larry Wos:
The Problem of Extending the Set of Support Strategy. J. Autom. Reason. 3(3): 319-328 (1987) - [j11]Larry Wos:
The Problem of Definition Expansion and Contraction. J. Autom. Reason. 3(4): 433-435 (1987) - 1986
- [j10]Robert S. Boyer, Ewing L. Lusk, William McCune, Ross A. Overbeek, Mark E. Stickel, Larry Wos:
Set Theory in First-Order Logic: Clauses for Gödel's Axioms. J. Autom. Reason. 2(3): 287-327 (1986) - [c9]Larry Wos, William McCune:
Negative Paramodulation. CADE 1986: 229-239 - 1985
- [j9]Larry Wos:
Editorial: A Journal Is Born. J. Autom. Reason. 1(1): 1-3 (1985) - [j8]Larry Wos:
What Is Automated Reasoning? J. Autom. Reason. 1(1): 6-9 (1985) - 1984
- [j7]Larry Wos, Steve Winker, Barry Smith, Robert Veroff, Lawrence J. Henschen:
A New Use of an Automated Reasoning Assistant: Open Questions in Equivalential Calculus and the Study of Infinite Domains. Artif. Intell. 22(3): 303-356 (1984) - [c8]Larry Wos, Robert Veroff, Barry Smith, William McCune:
The Linked Inference Principle, II: The User's Viewpoint. CADE 1984: 316-332 - 1983
- [j6]Larry Henschen, Barry Smith, Robert Veroff, Steve Winker, Larry Wos:
Questions concerning possible shortest single axioms for the equivalential calculus: an application of automated theorem proving to infinite domains. Notre Dame J. Formal Log. 24(2): 205-223 (1983) - [c7]Larry Wos:
Automated Reasoning: Real Uses and Potential Uses. IJCAI 1983: 867-876 - 1982
- [c6]Larry Wos:
Solving Open Questions with an Automated Theorem-Proving Program. CADE 1982: 1-31 - [c5]Steven K. Winker, Larry Wos:
Procedure Implementation Through Demodulation and Related Tricks. CADE 1982: 109-131 - 1981
- [c4]Larry Wos, Steven K. Winker, Ewing L. Lusk:
An automated reasoning system. AFIPS National Computer Conference 1981: 697-702 - 1980
- [c3]Larry Wos, Ross A. Overbeek, Lawrence J. Henschen:
Hyperparamodulation: A Refinement of Paramodulation. CADE 1980: 208-219
1970 – 1979
- 1978
- [c2]Steve Winker, Larry Wos:
Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra. MVL 1978: 251-256 - 1976
- [j5]John D. McCharen, Ross A. Overbeek, Larry Wos:
Problems and Experiments for and with Automated Theorem-Proving Programs. IEEE Trans. Computers 25(8): 773-782 (1976) - 1974
- [j4]Lawrence J. Henschen, Ross A. Overbeek, Larry Wos:
A Theorem-Proving Language for Experimentation. Commun. ACM 17(6): 308-314 (1974) - [j3]Lawrence J. Henschen, Larry Wos:
Unit Refutations and Horn Sets. J. ACM 21(4): 590-605 (1974)
1960 – 1969
- 1967
- [j2]Larry Wos, George A. Robinson, Daniel F. Carson, Leon Shalla:
The Concept of Demodulation in Theorem Proving. J. ACM 14(4): 698-709 (1967) - 1965
- [j1]Larry Wos, George A. Robinson, Daniel F. Carson:
Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. J. ACM 12(4): 536-541 (1965) - 1964
- [c1]Larry Wos, Daniel F. Carson, George A. Robinson:
The unit preference strategy in theorem proving. AFIPS Fall Joint Computing Conference (1) 1964: 615-621
Coauthor Index
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.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-09 13:21 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: