default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: William McCune
@inproceedings{DBLP:conf/aisc/McCune06,
author = {William McCune},
editor = {Jacques Calmet and
Tetsuo Ida and
Dongming Wang},
title = {Semantic Guidance for Saturation Provers},
booktitle = {Artificial Intelligence and Symbolic Computation, 8th International
Conference, {AISC} 2006, Beijing, China, September 20-22, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4120},
pages = {18--24},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11856290\_4},
doi = {10.1007/11856290\_4},
timestamp = {Wed, 20 Nov 2019 09:49:02 +0100},
biburl = {https://dblp.org/rec/conf/aisc/McCune06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:conf/tphol/BeesonM06,
author = {Michael Beeson and
William McCune},
editor = {Freek Wiedijk},
title = {Otter/Ivy},
booktitle = {The Seventeen Provers of the World, Foreword by Dana S. Scott},
series = {Lecture Notes in Computer Science},
volume = {3600},
pages = {36--40},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11542384\_7},
doi = {10.1007/11542384\_7},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/BeesonM06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0402010,
author = {Olga Shumsky Matlin and
William McCune},
title = {Encapsulation for Practical Simplification Procedures},
journal = {CoRR},
volume = {cs.LO/0402010},
year = {2004},
url = {http://arxiv.org/abs/cs/0402010},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-LO-0402010.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0312012,
author = {Olga Shumsky Matlin and
William McCune and
Ewing L. Lusk},
title = {Methods to Model-Check Parallel Systems Software},
journal = {CoRR},
volume = {cs.LO/0312012},
year = {2003},
url = {http://arxiv.org/abs/cs/0312012},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-LO-0312012.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-SC-0310055,
author = {William McCune},
title = {Mace4 Reference Manual and Guide},
journal = {CoRR},
volume = {cs.SC/0310055},
year = {2003},
url = {http://arxiv.org/abs/cs/0310055},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-SC-0310055.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-SC-0310056,
author = {William McCune},
title = {{OTTER} 3.3 Reference Manual},
journal = {CoRR},
volume = {cs.SC/0310056},
year = {2003},
url = {http://arxiv.org/abs/cs/0310056},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-SC-0310056.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCuneVFHFW02,
author = {William McCune and
Robert Veroff and
Branden Fitelson and
Kenneth Harris and
Andrew Feist and
Larry Wos},
title = {Short Single Axioms for Boolean Algebra},
journal = {J. Autom. Reason.},
volume = {29},
number = {1},
pages = {1--16},
year = {2002},
url = {https://doi.org/10.1023/A:1020542009983},
doi = {10.1023/A:1020542009983},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCuneVFHFW02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/spin/MatlinLM02,
author = {Olga Shumsky Matlin and
Ewing L. Lusk and
William McCune},
editor = {Dragan Bosnacki and
Stefan Leue},
title = {SPINning Parallel Systems Software},
booktitle = {Model Checking of Software, 9th International {SPIN} Workshop, Grenoble,
France, April 11-13, 2002, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2318},
pages = {213--220},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-46017-9\_16},
doi = {10.1007/3-540-46017-9\_16},
timestamp = {Tue, 14 May 2019 10:00:36 +0200},
biburl = {https://dblp.org/rec/conf/spin/MatlinLM02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0203009,
author = {Olga Shumsky Matlin and
Ewing L. Lusk and
William McCune},
title = {SPINning Parallel Systems Software},
journal = {CoRR},
volume = {cs.LO/0203009},
year = {2002},
url = {https://arxiv.org/abs/cs/0203009},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-LO-0203009.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0106042,
author = {William McCune},
title = {{MACE} 2.0 Reference Manual and Guide},
journal = {CoRR},
volume = {cs.LO/0106042},
year = {2001},
url = {https://arxiv.org/abs/cs/0106042},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-LO-0106042.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/McCuneS00,
author = {William McCune and
Olga Shumsky},
editor = {David A. McAllester},
title = {System Description: {IVY}},
booktitle = {Automated Deduction - CADE-17, 17th International Conference on Automated
Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1831},
pages = {401--405},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/10721959\_30},
doi = {10.1007/10721959\_30},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/McCuneS00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ipl/McCune98,
author = {William McCune},
title = {Automatic Proofs and Counterexamples for Some Ortholattice Identities},
journal = {Inf. Process. Lett.},
volume = {65},
number = {6},
pages = {285--291},
year = {1998},
url = {https://doi.org/10.1016/S0020-0190(98)00015-5},
doi = {10.1016/S0020-0190(98)00015-5},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/ipl/McCune98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCuneW97,
author = {William McCune and
Larry Wos},
title = {Otter - The {CADE-13} Competition Incarnations},
journal = {J. Autom. Reason.},
volume = {18},
number = {2},
pages = {211--220},
year = {1997},
url = {https://doi.org/10.1023/A:1005843632307},
doi = {10.1023/A:1005843632307},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCuneW97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCune97,
author = {William McCune},
title = {Solution of the Robbins Problem},
journal = {J. Autom. Reason.},
volume = {19},
number = {3},
pages = {263--276},
year = {1997},
url = {https://doi.org/10.1023/A:1005843212881},
doi = {10.1023/A:1005843212881},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCune97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/McCune97,
author = {William McCune},
editor = {Hubert Comon},
title = {Well-Behaved Search and the Robbins Problem},
booktitle = {Rewriting Techniques and Applications, 8th International Conference,
RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1232},
pages = {1--7},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-62950-5\_57},
doi = {10.1007/3-540-62950-5\_57},
timestamp = {Tue, 14 May 2019 10:00:46 +0200},
biburl = {https://dblp.org/rec/conf/rta/McCune97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sac/ShumskyWME97,
author = {Olga Shumsky and
Ralph W. Wilkerson and
William McCune and
Fikret Er{\c{c}}al},
editor = {Barrett R. Bryant and
Janice H. Carroll and
Dave Oppenheim and
Jim Hightower and
K. M. George},
title = {Direct finite first-order model generation with negative constraint
propagation heuristic},
booktitle = {Proceedings of the 1997 {ACM} symposium on Applied Computing, SAC'97,
San Jose, CA, USA, February 28 - March 1},
pages = {25--29},
publisher = {{ACM}},
year = {1997},
url = {https://doi.org/10.1145/331697.331704},
doi = {10.1145/331697.331704},
timestamp = {Tue, 06 Nov 2018 11:06:49 +0100},
biburl = {https://dblp.org/rec/conf/sac/ShumskyWME97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/1997,
editor = {William McCune},
title = {Automated Deduction - CADE-14, 14th International Conference on Automated
Deduction, Townsville, North Queensland, Australia, July 13-17, 1997,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1249},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-63104-6},
doi = {10.1007/3-540-63104-6},
isbn = {3-540-63104-6},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/1997.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/sp/McCuneP96,
author = {William McCune and
R. Padmanabhan},
title = {Automated Deduction in Equational Logic and Cubic Curves},
series = {Lecture Notes in Computer Science},
volume = {1095},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61398-6},
doi = {10.1007/3-540-61398-6},
isbn = {3-540-61398-6},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/sp/McCuneP96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/SlaneyLM94,
author = {John K. Slaney and
Ewing L. Lusk and
William McCune},
editor = {Alan Bundy},
title = {{SCOTT:} Semantically Constrained Otter System Description},
booktitle = {Automated Deduction - CADE-12, 12th International Conference on Automated
Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {814},
pages = {764--768},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-58156-1\_56},
doi = {10.1007/3-540-58156-1\_56},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/SlaneyLM94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BonacinaM94,
author = {Maria Paola Bonacina and
William McCune},
editor = {Alan Bundy},
title = {Distributed Theorem Proving by Peers},
booktitle = {Automated Deduction - CADE-12, 12th International Conference on Automated
Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {814},
pages = {841--845},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-58156-1\_72},
doi = {10.1007/3-540-58156-1\_72},
timestamp = {Sat, 20 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BonacinaM94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCune93,
author = {William McCune},
title = {Single Axioms for Groups and Abelian Groups with Various Operations},
journal = {J. Autom. Reason.},
volume = {10},
number = {1},
pages = {1--13},
year = {1993},
url = {https://doi.org/10.1007/BF00881862},
doi = {10.1007/BF00881862},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCune93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/LuskM93,
author = {Ewing L. Lusk and
William McCune},
title = {Uniform Strategies: The {CADE-11} Theorem Proving Contest},
journal = {J. Autom. Reason.},
volume = {11},
number = {3},
pages = {317--331},
year = {1993},
url = {https://doi.org/10.1007/BF00881871},
doi = {10.1007/BF00881871},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/LuskM93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ndjfl/McCune93,
author = {William McCune},
title = {Single Axioms for the Left Group and the Right Group Calculi},
journal = {Notre Dame J. Formal Log.},
volume = {34},
number = {1},
pages = {132--139},
year = {1993},
url = {https://doi.org/10.1305/ndjfl/1093634569},
doi = {10.1305/NDJFL/1093634569},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ndjfl/McCune93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/amai/WosM92,
author = {Larry Wos and
William McCune},
title = {The Application of Automated Reasoning to Questions in Mathematics
and Logic},
journal = {Ann. Math. Artif. Intell.},
volume = {5},
number = {2-4},
pages = {321--369},
year = {1992},
url = {https://doi.org/10.1007/BF01543481},
doi = {10.1007/BF01543481},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/amai/WosM92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCune92,
author = {William McCune},
title = {Automated Discovery of New Axiomatizations of the Left Group and Right
Group Calculi},
journal = {J. Autom. Reason.},
volume = {9},
number = {1},
pages = {1--24},
year = {1992},
url = {https://doi.org/10.1007/BF00247824},
doi = {10.1007/BF00247824},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCune92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCune92a,
author = {William McCune},
title = {Experiments with Discrimination-Tree Indexing and Path Indexing for
Term Retrieval},
journal = {J. Autom. Reason.},
volume = {9},
number = {2},
pages = {147--167},
year = {1992},
url = {https://doi.org/10.1007/BF00245458},
doi = {10.1007/BF00245458},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCune92a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/McCuneW92,
author = {William McCune and
Larry Wos},
editor = {Deepak Kapur},
title = {Experiments in Automated Deduction with Condensed Detachment},
booktitle = {Automated Deduction - CADE-11, 11th International Conference on Automated
Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {607},
pages = {209--223},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-55602-8\_167},
doi = {10.1007/3-540-55602-8\_167},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/McCuneW92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/LuskMS92,
author = {Ewing L. Lusk and
William McCune and
John K. Slaney},
editor = {Deepak Kapur},
title = {{ROO:} {A} Parallel Theorem Prover},
booktitle = {Automated Deduction - CADE-11, 11th International Conference on Automated
Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {607},
pages = {731--734},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-55602-8\_213},
doi = {10.1007/3-540-55602-8\_213},
timestamp = {Sat, 20 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/LuskMS92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/McCuneW92,
author = {William McCune and
Larry Wos},
editor = {Andrei Voronkov},
title = {Application of Automated Deduction to the Search for Single Axioms
for Exponent Groups},
booktitle = {Logic Programming and Automated Reasoning,International Conference
LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {624},
pages = {131--136},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/BFb0013055},
doi = {10.1007/BFB0013055},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/McCuneW92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jlp/WosM91,
author = {Larry Wos and
William McCune},
title = {Automated Theorem Proving and Logic Programming},
journal = {J. Log. Program.},
volume = {11},
number = {1{\&}2},
pages = {1--53},
year = {1991},
url = {https://doi.org/10.1016/0743-1066(91)90008-D},
doi = {10.1016/0743-1066(91)90008-D},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jlp/WosM91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/McCuneW91,
author = {William McCune and
Larry Wos},
title = {The Absence and the Presence of Fixed Point Combinators},
journal = {Theor. Comput. Sci.},
volume = {87},
number = {1},
pages = {221--228},
year = {1991},
url = {https://doi.org/10.1016/0304-3975(91)90034-Y},
doi = {10.1016/0304-3975(91)90034-Y},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcs/McCuneW91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aaai/McCune90,
author = {William McCune},
editor = {Howard E. Shrobe and
Thomas G. Dietterich and
William R. Swartout},
title = {Skolem Functions and Equality in Automated Deduction},
booktitle = {Proceedings of the 8th National Conference on Artificial Intelligence.
Boston, Massachusetts, USA, July 29 - August 3, 1990, 2 Volumes},
pages = {246--251},
publisher = {{AAAI} Press / The {MIT} Press},
year = {1990},
url = {http://www.aaai.org/Library/AAAI/1990/aaai90-038.php},
timestamp = {Mon, 04 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/aaai/McCune90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/WosWMOLSB90,
author = {Larry Wos and
Steve Winker and
William McCune and
Ross A. Overbeek and
Ewing L. Lusk and
Rick L. Stevens and
Ralph Butler},
editor = {Mark E. Stickel},
title = {Automated Reasoning Contributed to Mathematics and Logic},
booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
FRG, July 24-27, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {485--499},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-52885-7\_109},
doi = {10.1007/3-540-52885-7\_109},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/WosWMOLSB90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/McCune90,
author = {William McCune},
editor = {Mark E. Stickel},
title = {{OTTER} 2.0},
booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
FRG, July 24-27, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {663--664},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-52885-7\_131},
doi = {10.1007/3-540-52885-7\_131},
timestamp = {Fri, 19 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/McCune90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/LuskM90,
author = {Ewing L. Lusk and
William McCune},
editor = {Mark E. Stickel},
title = {Tutorial on High-Performance Automated Theorem Proving},
booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
FRG, July 24-27, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {681},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-52885-7\_140},
doi = {10.1007/3-540-52885-7\_140},
timestamp = {Fri, 19 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/LuskM90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/LuskM90,
author = {Ewing L. Lusk and
William McCune},
editor = {Bertram Fronh{\"{o}}fer and
Graham Wrightson},
title = {Experiments with {ROO:} {A} Parallel Automated Deduction System},
booktitle = {Parallelization in Inference Systems, International Workshop, Dagstuhl
Castle, Germany, December 17-18, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {590},
pages = {139--162},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-55425-4\_6},
doi = {10.1007/3-540-55425-4\_6},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/LuskM90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/LuskMS90,
author = {Ewing L. Lusk and
William McCune and
John K. Slaney},
editor = {Bertram Fronh{\"{o}}fer and
Graham Wrightson},
title = {Parallel Closure-Based Automated Reasoning},
booktitle = {Parallelization in Inference Systems, International Workshop, Dagstuhl
Castle, Germany, December 17-18, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {590},
pages = {347},
publisher = {Springer},
year = {1990},
timestamp = {Thu, 25 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dagstuhl/LuskMS90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jacm/McCuneH89,
author = {William McCune and
Lawrence J. Henschen},
title = {Maintaining state constraints in relational databases: a proof theoretic
basis},
journal = {J. {ACM}},
volume = {36},
number = {1},
pages = {46--68},
year = {1989},
url = {https://doi.org/10.1145/58562.59302},
doi = {10.1145/58562.59302},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jacm/McCuneH89.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/WickM89,
author = {Cynthia A. Wick and
William McCune},
title = {Automated Reasoning about Elementary Point-Set Topology},
journal = {J. Autom. Reason.},
volume = {5},
number = {2},
pages = {239--255},
year = {1989},
url = {https://doi.org/10.1007/BF00243005},
doi = {10.1007/BF00243005},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/WickM89.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ipl/McCune88,
author = {William McCune},
title = {Un-Skolemizing Clause Sets},
journal = {Inf. Process. Lett.},
volume = {29},
number = {5},
pages = {257--263},
year = {1988},
url = {https://doi.org/10.1016/0020-0190(88)90119-6},
doi = {10.1016/0020-0190(88)90119-6},
timestamp = {Fri, 26 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ipl/McCune88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/McCune88,
author = {William McCune},
editor = {Ewing L. Lusk and
Ross A. Overbeek},
title = {Challenge Equality Problems in Lattice Theory},
booktitle = {9th International Conference on Automated Deduction, Argonne, Illinois,
USA, May 23-26, 1988, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {310},
pages = {704--709},
publisher = {Springer},
year = {1988},
url = {https://doi.org/10.1007/BFb0012868},
doi = {10.1007/BFB0012868},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/McCune88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/WosM88,
author = {Larry Wos and
William McCune},
editor = {Ewing L. Lusk and
Ross A. Overbeek},
title = {Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating
Automated Theorem-Proving Programs},
booktitle = {9th International Conference on Automated Deduction, Argonne, Illinois,
USA, May 23-26, 1988, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {310},
pages = {714--729},
publisher = {Springer},
year = {1988},
url = {https://doi.org/10.1007/BFb0012870},
doi = {10.1007/BFB0012870},
timestamp = {Fri, 19 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/WosM88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCuneW87,
author = {William McCune and
Larry Wos},
title = {A Case Study in Automated Theorem Proving: Finding Sages in Combinatory
Logic},
journal = {J. Autom. Reason.},
volume = {3},
number = {1},
pages = {91--107},
year = {1987},
url = {https://doi.org/10.1007/BF00381147},
doi = {10.1007/BF00381147},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCuneW87.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BoyerLMOSW86,
author = {Robert S. Boyer and
Ewing L. Lusk and
William McCune and
Ross A. Overbeek and
Mark E. Stickel and
Larry Wos},
title = {Set Theory in First-Order Logic: Clauses for G{\"{o}}del's Axioms},
journal = {J. Autom. Reason.},
volume = {2},
number = {3},
pages = {287--327},
year = {1986},
url = {https://doi.org/10.1007/BF02328452},
doi = {10.1007/BF02328452},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BoyerLMOSW86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/WosM86,
author = {Larry Wos and
William McCune},
editor = {J{\"{o}}rg H. Siekmann},
title = {Negative Paramodulation},
booktitle = {8th International Conference on Automated Deduction, Oxford, England,
July 27 - August 1, 1986, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {230},
pages = {229--239},
publisher = {Springer},
year = {1986},
url = {https://doi.org/10.1007/3-540-16780-3\_93},
doi = {10.1007/3-540-16780-3\_93},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/WosM86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ButlerLMO86,
author = {Ralph Butler and
Ewing L. Lusk and
William McCune and
Ross A. Overbeek},
editor = {J{\"{o}}rg H. Siekmann},
title = {Paths to High-Performance Automated Theorem Proving},
booktitle = {8th International Conference on Automated Deduction, Oxford, England,
July 27 - August 1, 1986, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {230},
pages = {588--597},
publisher = {Springer},
year = {1986},
url = {https://doi.org/10.1007/3-540-16780-3\_123},
doi = {10.1007/3-540-16780-3\_123},
timestamp = {Fri, 19 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/ButlerLMO86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/LuskMO86,
author = {Ewing L. Lusk and
William McCune and
Ross A. Overbeek},
editor = {J{\"{o}}rg H. Siekmann},
title = {{ITP} at Argonne National Laboratory},
booktitle = {8th International Conference on Automated Deduction, Oxford, England,
July 27 - August 1, 1986, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {230},
pages = {697--698},
publisher = {Springer},
year = {1986},
url = {https://doi.org/10.1007/3-540-16780-3\_143},
doi = {10.1007/3-540-16780-3\_143},
timestamp = {Fri, 19 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/LuskMO86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iclp/ButlerLMO86,
author = {Ralph Butler and
Ewing L. Lusk and
William McCune and
Ross A. Overbeek},
editor = {Ehud Shapiro},
title = {Parallel Logic Programming for Numeric Applications},
booktitle = {Third International Conference on Logic Programming, Imperial College
of Science and Technology, London, United Kingdom, July 14-18, 1986,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {225},
pages = {375--388},
publisher = {Springer},
year = {1986},
url = {https://doi.org/10.1007/3-540-16492-8\_88},
doi = {10.1007/3-540-16492-8\_88},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/iclp/ButlerLMO86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/McCuneH85,
author = {William McCune and
Lawrence J. Henschen},
title = {Experiments with Semantic Paramodulation},
journal = {J. Autom. Reason.},
volume = {1},
number = {3},
pages = {231--261},
year = {1985},
url = {https://doi.org/10.1007/BF00244271},
doi = {10.1007/BF00244271},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/McCuneH85.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/WosVSM84,
author = {Larry Wos and
Robert Veroff and
Barry Smith and
William McCune},
editor = {Robert E. Shostak},
title = {The Linked Inference Principle, {II:} The User's Viewpoint},
booktitle = {7th International Conference on Automated Deduction, Napa, California,
USA, May 14-16, 1984, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {170},
pages = {316--332},
publisher = {Springer},
year = {1984},
url = {https://doi.org/10.1007/978-0-387-34768-4\_19},
doi = {10.1007/978-0-387-34768-4\_19},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/WosVSM84.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/McCuneH83,
author = {William McCune and
Lawrence J. Henschen},
editor = {Alan Bundy},
title = {Semantic Paramodulation for Horn Sets},
booktitle = {Proceedings of the 8th International Joint Conference on Artificial
Intelligence. Karlsruhe, FRG, August 1983},
pages = {902--908},
publisher = {William Kaufmann},
year = {1983},
url = {http://ijcai.org/Proceedings/83-2/Papers/069.pdf},
timestamp = {Tue, 20 Aug 2019 16:18:54 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/McCuneH83.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/adbt/HenschenMN82,
author = {Lawrence J. Henschen and
William McCune and
Shamim A. Naqvi},
editor = {Herv{\'{e}} Gallaire and
Jean{-}Marie Nicolas and
Jack Minker},
title = {Compiling Constraint-Checking Programs from First-Order Formulas},
booktitle = {Advances in Data Base Theory, Vol. 2, Based on the Proceedings of
the Workshop on Logical Data Bases, December 14-17, 1982, Centre d'{\'{e}}tudes
et de recherches de Toulouse, France},
series = {Advances in Data Base Theory},
pages = {145--169},
publisher = {Plemum Press},
address = {New York},
year = {1982},
timestamp = {Thu, 29 Mar 2018 16:54:19 +0200},
biburl = {https://dblp.org/rec/conf/adbt/HenschenMN82.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/LuskMO82,
author = {Ewing L. Lusk and
William McCune and
Ross A. Overbeek},
editor = {Donald W. Loveland},
title = {Logic Machine Architecture: Kernel Funtions},
booktitle = {6th Conference on Automated Deduction, New York, USA, June 7-9, 1982,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {138},
pages = {70--84},
publisher = {Springer},
year = {1982},
url = {https://doi.org/10.1007/BFb0000052},
doi = {10.1007/BFB0000052},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/LuskMO82.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/LuskMO82a,
author = {Ewing L. Lusk and
William McCune and
Ross A. Overbeek},
editor = {Donald W. Loveland},
title = {Logic Machine Architecture: Inference Mechanisms},
booktitle = {6th Conference on Automated Deduction, New York, USA, June 7-9, 1982,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {138},
pages = {85--108},
publisher = {Springer},
year = {1982},
url = {https://doi.org/10.1007/BFb0000053},
doi = {10.1007/BFB0000053},
timestamp = {Fri, 19 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/LuskMO82a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-01-21 00:09 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
