Travelled to:1 × France
1 × Spain
1 × United Kingdom
5 × USA
Collaborated with:E.L.Lusk L.Wos R.A.Overbeek ∅ O.Shumsky J.K.Slaney R.Butler M.P.Bonacina R.W.Wilkerson F.Erçal R.Veroff B.Smith S.Winker R.L.Stevens
Talks about:theorem (5) logic (5) autom (5) prove (4) problem (3) architectur (2) parallel (2) descript (2) challeng (2) program (2)
Person: William McCune
DBLP: McCune:William
Facilitated 1 volumes:
EdContributed to:
2000
1997
199719941992199019881986
198619841982Wrote 19 papers:
- CADE-2000-McCuneS
- System Description: IVY (WM, OS), pp. 401–405.
- RTA-1997-McCune #problem
- Well-Behaved Search and the Robbins Problem (WM), pp. 1–7.
- SAC-1997-ShumskyWME #constraints #finite #first-order #generative #heuristic
- Direct finite first-order model generation with negative constraint propagation heuristic (OS, RWW, WM, FE), pp. 25–29.
- CADE-1994-BonacinaM #distributed #proving #theorem proving
- Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.
- CADE-1994-SlaneyLM #named #semantics
- SCOTT: Semantically Constrained Otter System Description (JKS, ELL, WM), pp. 764–768.
- CADE-1992-LuskMS #named #parallel #proving #theorem proving
- ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.
- CADE-1992-McCuneW #automation #deduction
- Experiments in Automated Deduction with Condensed Detachment (WM, LW), pp. 209–223.
- CADE-1990-LuskM #automation #proving #theorem proving #tutorial
- Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.
- CADE-1990-McCune
- OTTER 2.0 (WM), pp. 663–664.
- 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-McCune #challenge #problem #similarity
- Challenge Equality Problems in Lattice Theory (WM), pp. 704–709.
- 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-ButlerLMO #automation #proving #theorem proving
- Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
- CADE-1986-LuskMO
- ITP at Argonne National Laboratory (ELL, WM, RAO), pp. 697–698.
- CADE-1986-WosM
- Negative Paramodulation (LW, WM), pp. 229–239.
- ICLP-1986-ButlerLMO86 #logic programming #parallel
- Parallel Logic Programming for Numeric Applications (RB, ELL, WM, RAO), pp. 375–388.
- CADE-1984-WosVSM
- The Linked Inference Principle, II: The User’s Viewpoint (LW, RV, BS, WM), pp. 316–332.
- CADE-1982-LuskMO #architecture #kernel #logic
- Logic Machine Architecture: Kernel Funtions (ELL, WM, RAO), pp. 70–84.
- CADE-1982-LuskMO82a #architecture #logic
- Logic Machine Architecture: Inference Mechanisms (ELL, WM, RAO), pp. 85–108.