Travelled to:1 × Austria
1 × France
4 × USA
Collaborated with:W.McCune ∅ E.L.Lusk M.Beeson S.K.Winker R.A.Overbeek L.J.Henschen R.Veroff B.Smith S.Winker R.L.Stevens R.Butler
Talks about:autom (5) logic (3) paramodul (2) theorem (2) program (2) problem (2) reason (2) prove (2) equal (2) hyperparamodul (1)
Person: Larry Wos
DBLP: Wos:Larry
Contributed to:
2014
1992199019881986198419821980Wrote 11 papers:
- IJCAR-2014-BeesonW #geometry #proving
- OTTER Proofs in Tarskian Geometry (MB, LW), pp. 495–510.
- CADE-1992-LuskW #benchmark #metric #problem #similarity
- Benchmark Problems in Which Equality Plays the Major Role (ELL, LW), pp. 781–785.
- CADE-1992-McCuneW #automation #deduction
- Experiments in Automated Deduction with Condensed Detachment (WM, LW), pp. 209–223.
- CADE-1992-Wos #automation #logic #reasoning
- The Impossibility of the Automation of Logical Reasoning (LW), pp. 1–3.
- CADE-1990-WosWMOLSB #automation #logic #reasoning
- Automated Reasoning Contributed to Mathematics and Logic (LW, SW, WM, RAO, ELL, RLS, RB), pp. 485–499.
- CADE-1988-WosM #automation #challenge #combinator #logic #problem #similarity #source code
- Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs (LW, WM), pp. 714–729.
- CADE-1986-WosM
- Negative Paramodulation (LW, WM), pp. 229–239.
- CADE-1984-WosVSM
- The Linked Inference Principle, II: The User’s Viewpoint (LW, RV, BS, WM), pp. 316–332.
- CADE-1982-WinkerW #implementation
- Procedure Implementation Through Demodulation and Related Tricks (SKW, LW), pp. 109–131.
- CADE-1982-Wos #automation
- Solving Open Questions with an Automated Theorem-Proving Program (LW), pp. 1–31.
- CADE-1980-WosOH #named #refinement
- Hyperparamodulation: A Refinement of Paramodulation (LW, RAO, LJH), pp. 208–219.