Search the dblp DataBase
William McCune :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Lawrence J. Henschen , William McCune , Shamim A. Naqvi Compiling Constraint-Checking Programs from First-Order Formulas. [Citation Graph (20, 0)][DBLP ] Advances in Data Base Theory, 1982, pp:145-169 [Conf ] William McCune , Lawrence J. Henschen Maintaining state constraints in relational databases: a proof theoretic basis. [Citation Graph (9, 0)][DBLP ] J. ACM, 1989, v:36, n:1, pp:46-68 [Journal ] William McCune Un-Skolemizing Clause Sets. [Citation Graph (1, 0)][DBLP ] Inf. Process. Lett., 1988, v:29, n:5, pp:257-263 [Journal ] William McCune Skolem Functions and Equality in Automated Deduction. [Citation Graph (0, 0)][DBLP ] AAAI, 1990, pp:246-251 [Conf ] William McCune Semantic Guidance for Saturation Provers. [Citation Graph (0, 0)][DBLP ] AISC, 2006, pp:18-24 [Conf ] Maria Paola Bonacina , William McCune Distributed Theorem Proving by Peers. [Citation Graph (0, 0)][DBLP ] CADE, 1994, pp:841-845 [Conf ] Ralph Butler , Ewing L. Lusk , William McCune , Ross A. Overbeek Paths to High-Performance Automated Theorem Proving. [Citation Graph (0, 0)][DBLP ] CADE, 1986, pp:588-597 [Conf ] Ewing L. Lusk , William McCune Tutorial on High-Performance Automated Theorem Proving. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:681- [Conf ] Ewing L. Lusk , William McCune , Ross A. Overbeek Logic Machine Architecture: Kernel Funtions. [Citation Graph (0, 0)][DBLP ] CADE, 1982, pp:70-84 [Conf ] Ewing L. Lusk , William McCune , Ross A. Overbeek Logic Machine Architecture: Inference Mechanisms. [Citation Graph (0, 0)][DBLP ] CADE, 1982, pp:85-108 [Conf ] Ewing L. Lusk , William McCune , Ross A. Overbeek ITP at Argonne National Laboratory. [Citation Graph (0, 0)][DBLP ] CADE, 1986, pp:697-698 [Conf ] Ewing L. Lusk , William McCune , John K. Slaney ROO: A Parallel Theorem Prover. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:731-734 [Conf ] William McCune Challenge Equality Problems in Lattice Theory. [Citation Graph (0, 0)][DBLP ] CADE, 1988, pp:704-709 [Conf ] William McCune OTTER 2.0. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:663-664 [Conf ] William McCune , Olga Shumsky System Description: IVY. [Citation Graph (0, 0)][DBLP ] CADE, 2000, pp:401-405 [Conf ] William McCune , Larry Wos Experiments in Automated Deduction with Condensed Detachment. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:209-223 [Conf ] John K. Slaney , Ewing L. Lusk , William McCune SCOTT: Semantically Constrained Otter System Description. [Citation Graph (0, 0)][DBLP ] CADE, 1994, pp:764-768 [Conf ] Larry Wos , William McCune Negative Paramodulation. [Citation Graph (0, 0)][DBLP ] CADE, 1986, pp:229-239 [Conf ] Larry Wos , William McCune Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. [Citation Graph (0, 0)][DBLP ] CADE, 1988, pp:714-729 [Conf ] Larry Wos , Robert Veroff , B. Smith , William McCune The Linked Inference Principle, II: The User's Viewpoint. [Citation Graph (0, 0)][DBLP ] CADE, 1984, pp:316-332 [Conf ] Larry Wos , S. Winker , William McCune , Ross A. Overbeek , Ewing L. Lusk , Rick L. Stevens , Ralph Butler Automated Reasoning Contributed to Mathematics and Logic. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:485-499 [Conf ] Ewing L. Lusk , William McCune Experiments with ROO: A Parallel Automated Deduction System. [Citation Graph (0, 0)][DBLP ] Dagstuhl Seminar on Parallelization in Inference Systems, 1990, pp:139-162 [Conf ] Ewing L. Lusk , William McCune , John K. Slaney Parallel Closure-Based Automated Reasoning. [Citation Graph (0, 0)][DBLP ] Dagstuhl Seminar on Parallelization in Inference Systems, 1990, pp:347- [Conf ] Ralph Butler , Ewing L. Lusk , William McCune , Ross A. Overbeek Parallel Logic Programming for Numeric Applications. [Citation Graph (0, 0)][DBLP ] ICLP, 1986, pp:375-388 [Conf ] William McCune , Lawrence J. Henschen Semantic Paramodula tion for Horn Sets. [Citation Graph (0, 0)][DBLP ] IJCAI, 1983, pp:902-908 [Conf ] William McCune , Larry Wos Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. [Citation Graph (0, 0)][DBLP ] LPAR, 1992, pp:131-136 [Conf ] William McCune Well-Behaved Search and the Robbins Problem. [Citation Graph (0, 0)][DBLP ] RTA, 1997, pp:1-7 [Conf ] Olga Shumsky , Ralph W. Wilkerson , William McCune , Fikret Erçal Direct finite first-order model generation with negative constraint propagation heuristic. [Citation Graph (0, 0)][DBLP ] SAC, 1997, pp:25-29 [Conf ] Olga Shumsky Matlin , Ewing L. Lusk , William McCune SPINning Parallel Systems Software. [Citation Graph (0, 0)][DBLP ] SPIN, 2002, pp:213-220 [Conf ] Michael Beeson , William McCune Otter/Ivy. [Citation Graph (0, 0)][DBLP ] The Seventeen Provers of the World, 2006, pp:36-40 [Conf ] Larry Wos , William McCune The Application of Automated Reasoning to Questions in Mathematics and Logic. [Citation Graph (0, 0)][DBLP ] Ann. Math. Artif. Intell., 1992, v:5, n:2-4, pp:321-369 [Journal ] William McCune MACE 2.0 Reference Manual and Guide [Citation Graph (0, 0)][DBLP ] CoRR, 2001, v:0, n:, pp:- [Journal ] Olga Shumsky Matlin , Ewing L. Lusk , William McCune SPINning Parallel Systems Software [Citation Graph (0, 0)][DBLP ] CoRR, 2002, v:0, n:, pp:- [Journal ] Olga Shumsky Matlin , William McCune , Ewing L. Lusk Methods to Model-Check Parallel Systems Software [Citation Graph (0, 0)][DBLP ] CoRR, 2003, v:0, n:, pp:- [Journal ] Olga Shumsky Matlin , William McCune Encapsulation for Practical Simplification Procedures [Citation Graph (0, 0)][DBLP ] CoRR, 2004, v:0, n:, pp:- [Journal ] William McCune Mace4 Reference Manual and Guide [Citation Graph (0, 0)][DBLP ] CoRR, 2003, v:0, n:, pp:- [Journal ] William McCune OTTER 3.3 Reference Manual [Citation Graph (0, 0)][DBLP ] CoRR, 2003, v:0, n:, pp:- [Journal ] William McCune Automatic Proofs and Counterexamples for Some Ortholattice Identities. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 1998, v:65, n:6, pp:285-291 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1986, v:2, n:3, pp:287-327 [Journal ] Ewing L. Lusk , William McCune Uniform Strategies: The CADE-11 Theorem Proving Contest. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1993, v:11, n:3, pp:317-331 [Journal ] William McCune Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1992, v:9, n:1, pp:1-24 [Journal ] William McCune Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1992, v:9, n:2, pp:147-167 [Journal ] William McCune Single Axioms for Groups and Abelian Groups with Various Operations. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1993, v:10, n:1, pp:1-13 [Journal ] William McCune Solution of the Robbins Problem. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1997, v:19, n:3, pp:263-276 [Journal ] William McCune , Lawrence J. Henschen Experiments with Semantic Paramodulation. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1985, v:1, n:3, pp:231-261 [Journal ] William McCune , Robert Veroff , Branden Fitelson , Kenneth Harris , Andrew Feist , Larry Wos Short Single Axioms for Boolean Algebra. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2002, v:29, n:1, pp:1-16 [Journal ] William McCune , Larry Wos A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1987, v:3, n:1, pp:91-107 [Journal ] William McCune , Larry Wos Otter - The CADE-13 Competition Incarnations. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1997, v:18, n:2, pp:211-220 [Journal ] Cynthia A. Wick , William McCune Automated Reasoning about Elementary Point-Set Topology. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1989, v:5, n:2, pp:239-255 [Journal ] Larry Wos , William McCune Automated Theorem Proving and Logic Programming. [Citation Graph (0, 0)][DBLP ] J. Log. Program., 1991, v:11, n:1&2, pp:1-53 [Journal ] William McCune Single Axioms for the Left Group and the Right Group Calculi. [Citation Graph (0, 0)][DBLP ] Notre Dame Journal of Formal Logic, 1993, v:34, n:1, pp:132-139 [Journal ] William McCune , Larry Wos The Absence and the Presence of Fixed Point Combinators. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1991, v:87, n:1, pp:221-228 [Journal ] Search in 0.003secs, Finished in 0.304secs