BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: McCune:William

Facilitated 1 volumes:

CADE 1997Ed

Contributed to:

CADE 20002000
RTA 19971997
SAC 19971997
CADE 19941994
CADE 19921992
CADE 19901990
CADE 19881988
CADE 19861986
ICLP 19861986
CADE 19841984
CADE 19821982

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.