William McCune

54 papers A* 2A 17B 2Misc 2Journal 24Unranked 5

Year	Rank	Type	Title / Venue / Authors
2006	—	`ch.`	Otter/Ivy. The Seventeen Provers of the World Michael Beeson, William McCune
2006	Misc	`conf`	Semantic Guidance for Saturation Provers. AISC William McCune
2004	J	`jnl`	Encapsulation for Practical Simplification Procedures CoRR Olga Shumsky Matlin, William McCune
2003	J	`jnl`	Mace4 Reference Manual and Guide CoRR William McCune
2003	J	`jnl`	Methods to Model-Check Parallel Systems Software CoRR Olga Shumsky Matlin, William McCune, Ewing L. Lusk
2003	J	`jnl`	OTTER 3.3 Reference Manual CoRR William McCune
2002	J	`jnl`	SPINning Parallel Systems Software CoRR Olga Shumsky Matlin, Ewing L. Lusk, William McCune
2002	—	`conf`	SPINning Parallel Systems Software. SPIN Olga Shumsky Matlin, Ewing L. Lusk, William McCune
2002	J	`jnl`	Short Single Axioms for Boolean Algebra. J. Autom. Reason. William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos
2001	J	`jnl`	MACE 2.0 Reference Manual and Guide CoRR William McCune
2000	A	`conf`	System Description: IVY. CADE William McCune, Olga Shumsky
1998	J	`jnl`	Automatic Proofs and Counterexamples for Some Ortholattice Identities. Inf. Process. Lett. William McCune
1997	A	`ed.`	Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings CADE William McCune
1997	Misc	`conf`	Direct finite first-order model generation with negative constraint propagation heuristic. SAC Olga Shumsky, Ralph W. Wilkerson, William McCune, Fikret Erçal
1997	J	`jnl`	Otter - The CADE-13 Competition Incarnations. J. Autom. Reason. William McCune, Larry Wos
1997	J	`jnl`	Solution of the Robbins Problem. J. Autom. Reason. William McCune
1997	—	`conf`	Well-Behaved Search and the Robbins Problem. RTA William McCune
1996	—	`book`	Automated Deduction in Equational Logic and Cubic Curves William McCune, R. Padmanabhan
1994	A	`conf`	Distributed Theorem Proving by Peers. CADE Maria Paola Bonacina, William McCune
1994	A	`conf`	SCOTT: Semantically Constrained Otter System Description. CADE John K. Slaney, Ewing L. Lusk, William McCune
1993	J	`jnl`	Single Axioms for Groups and Abelian Groups with Various Operations. J. Autom. Reason. William McCune
1993	J	`jnl`	Single Axioms for the Left Group and the Right Group Calculi. Notre Dame J. Formal Log. William McCune
1993	J	`jnl`	Uniform Strategies: The CADE-11 Theorem Proving Contest. J. Autom. Reason. Ewing L. Lusk, William McCune
1992	B	`conf`	Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. LPAR William McCune, Larry Wos
1992	J	`jnl`	Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi. J. Autom. Reason. William McCune
1992	A	`conf`	Experiments in Automated Deduction with Condensed Detachment. CADE William McCune, Larry Wos
1992	J	`jnl`	Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. J. Autom. Reason. William McCune
1992	A	`conf`	ROO: A Parallel Theorem Prover. CADE Ewing L. Lusk, William McCune, John K. Slaney
1992	J	`jnl`	The Application of Automated Reasoning to Questions in Mathematics and Logic. Ann. Math. Artif. Intell. Larry Wos, William McCune
1991	J	`jnl`	Automated Theorem Proving and Logic Programming. J. Log. Program. Larry Wos, William McCune
1991	J	`jnl`	The Absence and the Presence of Fixed Point Combinators. Theor. Comput. Sci. William McCune, Larry Wos
1990	A	`conf`	Automated Reasoning Contributed to Mathematics and Logic. CADE Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler
1990	—	`conf`	Experiments with ROO: A Parallel Automated Deduction System. Dagstuhl Seminar on Parallelization in Inference Systems Ewing L. Lusk, William McCune
1990	A	`conf`	OTTER 2.0. CADE William McCune
1990	—	`conf`	Parallel Closure-Based Automated Reasoning. Dagstuhl Seminar on Parallelization in Inference Systems Ewing L. Lusk, William McCune, John K. Slaney
1990	A*	`conf`	Skolem Functions and Equality in Automated Deduction. AAAI William McCune
1990	A	`conf`	Tutorial on High-Performance Automated Theorem Proving. CADE Ewing L. Lusk, William McCune
1989	J	`jnl`	Automated Reasoning about Elementary Point-Set Topology. J. Autom. Reason. Cynthia A. Wick, William McCune
1989	J	`jnl`	Maintaining state constraints in relational databases: a proof theoretic basis. J. ACM William McCune, Lawrence J. Henschen
1988	A	`conf`	Challenge Equality Problems in Lattice Theory. CADE William McCune
1988	A	`conf`	Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. CADE Larry Wos, William McCune
1988	J	`jnl`	Un-Skolemizing Clause Sets. Inf. Process. Lett. William McCune
1987	J	`jnl`	A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. J. Autom. Reason. William McCune, Larry Wos
1986	A	`conf`	ITP at Argonne National Laboratory. CADE Ewing L. Lusk, William McCune, Ross A. Overbeek
1986	A	`conf`	Negative Paramodulation. CADE Larry Wos, William McCune
1986	B	`conf`	Parallel Logic Programming for Numeric Applications. ICLP Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek
1986	A	`conf`	Paths to High-Performance Automated Theorem Proving. CADE Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek
1986	J	`jnl`	Set Theory in First-Order Logic: Clauses for Gödel's Axioms. J. Autom. Reason. Robert S. Boyer, Ewing L. Lusk, William McCune, Ross A. Overbeek, Mark E. Stickel, Larry Wos
1985	J	`jnl`	Experiments with Semantic Paramodulation. J. Autom. Reason. William McCune, Lawrence J. Henschen
1984	A	`conf`	The Linked Inference Principle, II: The User's Viewpoint. CADE Larry Wos, Robert Veroff, Barry Smith, William McCune
1983	A*	`conf`	Semantic Paramodulation for Horn Sets. IJCAI William McCune, Lawrence J. Henschen
1982	—	`conf`	Compiling Constraint-Checking Programs from First-Order Formulas. Advances in Data Base Theory Lawrence J. Henschen, William McCune, Shamim A. Naqvi
1982	A	`conf`	Logic Machine Architecture: Inference Mechanisms. CADE Ewing L. Lusk, William McCune, Ross A. Overbeek
1982	A	`conf`	Logic Machine Architecture: Kernel Funtions. CADE Ewing L. Lusk, William McCune, Ross A. Overbeek