Linked bibliography for the SEP article "Automated Reasoning" by Frederic Portoraro

This is an automatically generated and experimental page

If everything goes well, this page should display the bibliography of the aforementioned article as it appears in the Stanford Encyclopedia of Philosophy, but with links added to PhilPapers records and Google Scholar for your convenience. Some bibliographies are not going to be represented correctly or fully up to date. In general, bibliographies of recent works are going to be much better linked than bibliographies of primary literature and older works. Entries with PhilPapers records have links on their titles. A green link indicates that the item is available online at least partially.

This experiment has been authorized by the editors of the Stanford Encyclopedia of Philosophy. The original article and bibliography can be found here.

Alama, J., P. Oppenheimer, and E. Zalta, “Automating Leibniz’s Theory of Concepts”, CADE 25: Proceedings of the 25th International Conference on Automated Deduction, (Lecture Notes in Artificial Intelligence: Volume 9195), A. Felty and A. Middeldorp (eds.), Berlin: Springer, pp. 73–97. (Scholar)
Anderson, C. A., 1990, “Some Emendations of Gödel’s Ontological Proof”, Faith and Philosophy, 7(3): 291–303. (Scholar)
Anderson, A. R. and N. D. Belnap, 1962, “The Pure Calculus of Entailment”, Journal of Symbolic Logic, 27: 19–52. (Scholar)
Andrews, P. B., 1981, “Theorem-Proving via General Matings”, Journal of the Association for Computing Machinery, 28 (2): 193–214. (Scholar)
Andrews, P. B., M. Bishop and C. E. Brown, 2006, “TPS: A Hybrid Automatic-Interactive System for Developing Proofs”, Journal of Applied Logic, 4: 367–395. (Scholar)
Andrews, P. B., M. Bishop, S. Issar, D. Nesmith, F. Pfenning and H. Xi, 1996, “TPS: A Theorem-Proving System for Classical Type Theory”, Journal of Automated Reasoning, 16 (3): 321–353. (Scholar)
Appel, K., and W. Haken, 1977, “Every Planar Map is Four Colorable Part I. Discharging”, Illinois Journal of Mathematics, 21: 429–490. (Scholar)
Aransay, J., J. Divansón, 2017, “A Formalization in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem”, Journal of Automated Reasoning, 58 (4): 509–535. (Scholar)
Avigad, J. and J. Harrison, 2014, “Formally Verified Mathematics”, Communications of the ACM, 57 (4): 66–75. (Scholar)
Avigad, J., J. Hölzl and L. Serafin, 2017, “A Formally Verified Proof of the Central Limit Theorem”, Journal of Automated Reasoning, 59 (4): 389–423. (Scholar)
Baader, F. and T. Nipkow, 1998, Term Rewriting and All That, Cambridge: Cambridge University Press. (Scholar)
Bachmair, L. and H. Ganzinger, 1994, “Rewrite-Based Equational Theorem Proving with Selection and Simplification”, Journal of Logic and Computation, 4 (3): 217–247. (Scholar)
Ballarin, C., 2014, “Locales: A Module System for Mathematical Theories”, Journal of Automated Reasoning, 52 (2): 123–153. (Scholar)
Bancerek, G. and P. Rudnicki, 2003, “Information Retrieval in MML”, Proceedings of the Second International Conference on Mathematical Knowledge Management, LNCS 2594, Heidelberg: Springer-Verlag, pp. 119-132 (Scholar)
Bancerek, G., C. Byliński, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz and K. Pąk, 2018, “The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar”, Journal of Automated Reasoning (Special Issue: Milestones in Interactive Theorem Proving), 61 (9): 9–31. (Scholar)
Barret C., M. Deters, L. de Moura, A. Oliveras and A. Stump, 2013, “6 Years of SMT-COMP”, Journal of Automated Reasoning, 50 (3): 243–277. (Scholar)
Basin, D. A. and T. Walsh, 1996, “A Calculus for and Termination of Rippling”, Journal of Automated Reasoning, 16 (1–2): 147–180. (Scholar)
Bauer, A., E. Clarke and X. Zhao, 1998, “Analytica: An Experiment in Combining Theorem Proving and Symbolic Computation”, Journal of Automated Reasoning, 21: 295–325. (Scholar)
Beckert, B., R. Hanle and P.H. Schmitt (eds.), 2007, “Verification of Object-Oriented Software: The KeY Approach”, Lecture Notes in Artificial Intelligence (Volume 4334), Berlin: Springer-Verlag. (Scholar)
Beeson M., 2001, “Automatic Derivation of the Irrationality of e”, Journal of Symbolic Computation, 32 (4): 333–349. (Scholar)
Beeson,M. and L. Wos, 2017, “Finding Proofs in Tarskian Geometry”, Journal of Automated Reasoning, 58 (1), 181–207. (Scholar)
Bentkamp, A., J.C. Blanchette and D. Klakow, 2019, “A Formal Proof of the Expressiveness of Deep Learning”, Journal of Automated Reasoning, 63 (2), 347–368. (Scholar)
Bentkamp, A., J. Blanchette, S. Tourret, P. Vukmirović and U. Waldmann, 2021, “Superposition with Lambdas”, Journal of Automated Reasoning, 65 (7), 893–940. (Scholar)
Benzmüller, C., 2019, “Universal (Meta-) Logical Reasoning: Recent Successes”, Science of Computer Programming, Vol. 172, 48–62. (Scholar)
Benzmüller, C. and B. W. Paleo, 2014, “Automating Gödel’s Ontological Proof of God’s Existence with Higher-Order Automated Theorem Provers”, ECAI 2014: Proceedings of the 21st European Conference on Artificial Intelligence, T. Schaub et al. (eds.), IOS Press, pp. 93–98. (Scholar)
–––, 2015, “Higher-Order Modal Logics: Automation and Applications”, Reasoning Web 2015, LNCS 9203, W. Faber and A. Paschke (eds.), pp. 32–74. (Scholar)
Benzmüller C., X. Parent and L. van der Torre, 2018, “A Deontic Logic Reasoning Infrastructure”, CiE2018: Proceedings of the 14th Conference on Computability in Europe, LNCS 10936, F. Manea et al. (eds.), pp. 60–69. (Scholar)
Benzmüller C. and L. C. Paulson, 2013, “Quantified Multimodal Logics in Simple Type Theory”, Logica Universalis, 7 (1): 7–20. (Scholar)
Benzmüller, C. and D. S. Scott, 2020, “Automating Free Logic in HOL, with an Experimental Application in Category Theory”, Journal of Automated Reasoning, 64 (1), 53–72. (Scholar)
Benzmüller, C., A. Steen and M. Wisniewski, 2017, “Leo-III version 1.1 (system description)”, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)—Short Papers, T. Eiter, D. Sands, G. Sutcliffe and A. Voronkov (eds.), Kalpa Publications in Computing, Volume 1: 11–26. (Scholar)
Benzmüller, C., N. Sultana, L. C. Paulson and F. Theiß, 2015, “The Higher-Order Prover LEO-II”, Journal of Automated Reasoning, 55 (4): 389–404. (Scholar)
Berndt, B., 1985, Ramanujan’s Notebooks (Part I), Berlin: Springer-Verlag, pp. 25-43. (Scholar)
Beyer, D., M. Dangl and P. Wendler, 2018, “A Unifying View on SMT-Based Software Verification”, Journal of Automated Reasoning, 60 (3): 299–335. (Scholar)
Beyer, D., M. Dangl and P. Wendler, 2021, “Correction to: A Unifying View on SMT-Based Software Verification”, Journal of Automated Reasoning, 65 (3): 461. (Scholar)
Bibel, W., 1981, “On Matrices with Connections”, Journal of the Association of Computing Machinery, 28 (4): 633–645. (Scholar)
Blanchette, J. C., S. Böhme and L. C. Paulson, 2013, “Extending Sledgehammer with SMT Solvers”, Journal of Automated Reasoning, 51 (1): 109–128. (Scholar)
Blanchette, J. C. and T. Nipkow, 2010, “Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder”, ITP2010: First International Conference on Interactive Theorem Proving, LNCS 6172, M. Kaufmann and L. C. Paulson (eds.), pp. 131–146. (Scholar)
Bledsoe, W. W., 1977, “Non-resolution Theorem Proving”, Artificial Intelligence, 9: 1–35. (Scholar)
Bledsoe, W. W. and M. Tyson, 1975, “The UT Interactive Prover”, Memo ATP-17A, Department of Mathematics, University of Texas. (Scholar)
Boender, J., F. Kammüller and R. Nagarajan, 2015, “Formalization of Quantum Protocols using Coq”, 12th International Workshop on Quantum Physics and Logic (QPL), Oxford, arXiv preprint arXiv:1511.01568. (Scholar)
Bofill, M., R. Nieuwenhuis, A. Oliveras, E. Rodriguez-Carbonell and A. Rubio, 2008, “A Write-Based Solver for SAT Modulo the Theory of Arrays”, Formal Methods in Computer-Aided Design (FMCAD’08), pp. 1–8. (Scholar)
Bonacina, M. P., 1999, “A Taxonomy of Theorem-Proving Strategies”, Artificial Intelligence Today, (Lecture Notes in Computer Science: Volume 1600), Berlin: Springer-Verlag, pp. 43–84. (Scholar)
Bordg, A., H. Lachnitt and Y. He, 2021, “Certified Quantum Computation in Isabelle/HOL”, Journal of Automated Reasoning, 65 (5): 691–709. (Scholar)
Boyer R., et al., 1994, “The QED Manifesto”, CADE-12: Proceedings of the 12th International Conference on Automated Deduction, (Lecture Notes in Artificial Intelligence: Volume 814), A. Bundy (ed.), Berlin: Springer-Verlag, pp. 238–251. (Scholar)
Boyer, R. S., M. Kaufmann and J. S. Moore, 1995, “The Boyer-Moore Theorem Prover and its Interactive Enhancement”, Computers and Mathematics with Applications, 29: 27–62. (Scholar)
Boyer, R.S. and J. S. Moore, 1979, A Computational Logic, New York: Academic Press. (Scholar)
Brakensiek, J., M. Heule, J. Mackey and D. Narváez, 2022, “The Resolution of Keller’s Conjecture”, Journal of Automated Reasoning, 66 (3): 277–300. (Scholar)
Bridge, J.P., S.B. Holden and L.C. Paulson, 2014, “Machine Learning for First-Order Theorem Proving”, Journal of Automated Reasoning, 53 (2), 141–172. (Scholar)
Brown, C. E., 2012, “Satallax: An Automatic Higher-Order Prover”, Automated Reasoning: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), LNAI 7364, B. Gramlich et al. (eds.), pp. 111–117, Springer-Verlag. (Scholar)
–––, 2013, “Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems”, Journal of Automated Reasoning, 51 (1): 57–77. (Scholar)
Buchberger B., T. Jebelean, T. Kutsia, A. Maletzky and W. Windsteiger, 2016, “Theorema 2.0: Computer-Assisted Natural-Style Mathematics”, Journal of Formalized Reasoning, 9 (1): 149–185. (Scholar)
Bundy, A., 2011, “Automated theorem proving: a practical tool for the working mathematician?”, Annals of Mathematics and Artificial Intelligence, 61 (1): 3–14. (Scholar)
Bundy, A., F. van Harmelen, J. Hesketh and A. Smaill, 1991, “Experiments with Proof Plans for Induction”, Journal of Automated Reasoning, 7 (3): 303–324. (Scholar)
Bundy, A., A. Stevens, F. van Harmelen, A. Ireland and A. Smaill, 1993, “Rippling: A Heuristic for Guiding Inductive Proofs”, Artificial Intelligence, 62: 185–253. (Scholar)
Buresh-Oppenheim, J. and T. Pitassi, 2007, “The Complexity of Resolution Refinements”, Journal of Symbolic Logic, 72 (4): 1336–1352. (Scholar)
Chan, HL. and M. Norrish, 2019, “Classification of Finite Fields with Applications”, Journal of Automated Reasoning, 63 (3): 667–693. (Scholar)
Chang, C. L. and R. C. T. Lee, 1973, Symbolic Logic and Mechanical Theorem Proving, New York: Academic Press. (Scholar)
Chou, S., 1987, Mechanical Geometry Theorem Proving, Dordrecht: Kluwer Academic Publishers. (Scholar)
Church, A., 1936a, “An unsolvable problem of elementary number theory”, American Journal of Mathematics, 58 (2): 345–363. (Scholar)
–––, 1936b, “A note on the Entscheidungsproblem”, Journal of Symbolic Logic, 1 (1): 40–41. (Scholar)
–––, 1940, “A Formulation of the Simple Theory of Types”, Journal of Symbolic Logic, 5: 56–68. (Scholar)
Claessen, K. and N. Sörensson, 2003, “New Techniques that Improve MACE-style Finite Model Finding”, Proceedings of the CADE-19 Workshop: Model Computation – Principles, Algorithms, Applications, P. Baumgartner and C. Fermueller (eds.) (Scholar)
Clarke, E. and X. Zhao, 1994, “Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan”, CADE-12: Proceedings of the 12th International Conference on Automated Deduction, (Lecture Notes in Artificial Intelligence: Volume 814), A. Bundy (ed.), Berlin: Springer-Verlag, pp. 758-763. (Scholar)
Clocksin, W. F. and C. S. Mellish, 1981, Programming in Prolog, Berlin: Springer-Verlag. (Scholar)
Colmerauer, A., H. Kanoui, R. Pasero and P. Roussel, 1973, Un Système de Communication Homme-machine en Français, Rapport, Groupe Intelligence Artificielle, Université d’Aix Marseille. (Scholar)
Constable, R. L., S. F. Allen, H. M. Bromley, W.R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki and S. F. Smith, 1986, Implementing Mathematics with the Nuprl Proof Development System, Englewood Cliffs, NJ: Prentice Hall. (Scholar)
Cook, S. A., 1971, “The complexity of Theorem-Proving Procedures”, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, New York: Association for Computing Machinery, pp. 151–158. (Scholar)
Coquand, T. and G. Huet, 1988, “The Calculus of Constructions”, Information and Computation - Semantics of Data Types, A. R. Meyer (ed.), 76 (2–3): 95–120. (Scholar)
Coquand, T. and C. Paulin-Mohring, 1988, “Inductively Defined Types”, COLOG88: Proceedings of the International Conference on Computer Logic, P. Martin-Löf and G. Mints (eds.), LNCS 417, pp. 50–66. (Scholar)
Davis, M., G. Logemann and D. Loveland, 1962, “A Machine Program for Theorem-Proving”, Communications of the Association for Computing Machinery, 5 (7): 394–397. (Scholar)
Davis, M. and H. Putnam, 1960, “A Computing Procedure for Quantification Theory”, Journal of the Association for Computing Machinery, 7 (3): 201–215. (Scholar)
de Bruijn, N. G., 1968, “Automath, a Language for Mathematics”, in Automation of Reasoning (Volume 2), J. Siekmann and G. Wrighston (eds.), Berlin: Springer-Verlag, 1983, pp. 159–200. (Scholar)
de Moura, L., 2007, “Developing Efficient SMT Solvers”, Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, G. Sutcliffe, J. Urban and S. Schulz (eds.), Bremen. (Scholar)
Denney, E., B. Fischer and J. Schumann, 2004, “Using Automated Theorem Provers to Certify Auto-generated Aerospace Software”, Automated Reasoning, Second International Joint Conference (IJCAR) (Lecture Notes in Artificial Intelligence: Volume 3097), D. Basin and M. Rusinowitch (eds.), Berlin: Springer-Verlag, pp. 198-212. (Scholar)
Denney, E., J. Power and K. Tourlas, 2006, “Hiproofs: A Hierarchical Notion of Proof Tree”, Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI) (Electronic Notes in Theoretical Computer Science, Vol. 155), pp. 341–359. (Scholar)
Deutsch, D., 1982, “Quantum theory, the Church-Turing principle and the universal quantum computer”, Proceedings of the Royal Society of London A, 400: 97–117. (Scholar)
Dieks, D., 1982, “Communication by EPR devices”, Physics Letters A, 92: 271–272. (Scholar)
Eisert, J., M. Wilkens and M. Lewenstein, 1999, “Quantum games and quantum strategies”, Physical Review Letters, 83: 3077–3080. (Scholar)
–––, 2020, “Erratum: quantum games and quantum strategies”, [Physical Review Letters, 83: 3077–3080], Physical Review Letters, 124: 139901. (Scholar)
Ernst, Z., B. Fitelson, K. Harris and L. Wos, 2002, “Shortest Axiomatizations of Implicational S4 and S5”, Notre Dame Journal of Formal Logic, 43 (3): 169–179. (Scholar)
Farmer, W. M., J. D. Guttman and F. J. Thayer, 1993, “IMPS: An Interactive Mathematical Proof System”, Journal of Automated Reasoning, 11 (2): 213–248. (Scholar)
Fitelson B. and E. Zalta, 2007, “Steps Toward a Computational Metaphysics”, Journal of Philosophical Logic, 36 (2): 227–247. (Scholar)
Fitting, M., 1990, First-Order Logic and Automated Theorem Proving, Berlin: Springer-Verlag. (Scholar)
–––, 2002, Types, Tableaus and Gödel’s God. Kluwer. (Scholar)
Fuenmayor, D. and C. Benzmüller, 2017, “Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic”, KI 2017: Advances in Artificial Intelligence - Proceedings of the 40th Annual German Conference on AI, LNCS 10505, G. Kern-Isberner et al. (eds.), pp. 114-127. (Scholar)
Furbach , U., 1994, “Theory Reasoning in First Order Calculi”, Management and Processing of Complex Data Structures, (Lecture Notes in Computer Science Volume 777), pp. 139–156. (Scholar)
Furbach, U., C. Schon and F. Stolzenburg, 2014, “Automated Reasoning in Deontic Logic”, MIWAI2014: Proceedings of the 8th Multi-disciplinary International Workshop on Artificial Intelligence, LNAI 8875, M. N. Murty et al. (eds.), pp. 57–68. (Scholar)
Ganesalingam, M. and W. T. Gowers, 2017, “A Fully Automatic Theorem Prover with Human-Style Output”, Journal of Automated Reasoning, 58 (2): 253–291. (Scholar)
Ganzinger, H., G. Hagen, R. Nieuwenhuis, A. Oliveras, C. Tinelli, 2004, “DPLL(T): Fast Decision Procedures”, Computer Aided Verification, (Lecture Notes in Computer Science: Volume 3114), pp. 175–188. (Scholar)
Gentzen, G., 1935, “Investigations into Logical Deduction”, in Szabo 1969, pp. 68–131. (Scholar)
Giarratano, J. and G. Riley, 2004, Expert Systems: Principles and Programming, 4th edition, Boston, MA: PWS Publishing Co. (Scholar)
Gödel, K., 1970, “Appendix A: Notes in Kurt Gödel’s Hand“, in Sobel 2004, pp. 144–145. (Scholar)
Gordon, M. J. C. and T. F. Melham, eds., 1993, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge: Cambridge University Press. (Scholar)
Gordon, M. J. C., A. J. Milner and C. P. Wadsworth, 1979, Edinburgh LCF: A Mechanised Logic of Computation (LNCS 78), Berlin: Springer-Verlag. (Scholar)
Gorenstein, D., 1982, Finite Simple Groups: An Introduction to their Classification (University Series in Mathematics), New York: Plenum Press. (Scholar)
Green, C., 1969, “Application of Theorem Proving to Problem Solving”, IJCAI’69 Proceedings of the 1st international joint conference on Artificial intelligence, San Francisco: Morgan Kaufmann, pp. 219–239 (Scholar)
Haack, S., 1978, Philosophy of Logics, Cambridge: Cambridge University Press. (Scholar)
Hales, T. C., 2005a, “A proof of the Kepler Conjecture”, Annals of Mathematics, 162 (3): 1065–1185. (Scholar)
–––, 2006, “Introduction to the Flyspeck Project”, Dagstuhl Seminar Proceedings 05021: Mathematics, Algorithms, Proofs, T. Coquand et al. (eds.) (Scholar)
Hales, T. C. et al., 2015, “A Formal Proof of the Kepler Conjecture”, arXiv:1501.02.02155 9 [mat.MG], Cornell University Library. (Scholar)
Harrison, J., 2000, “High-Level Verification Using Theorem Proving and Formalized Mathematics”, CADE-17: Proceedings of the 17th International Conference on Automated Deduction, (Lecture Notes in Artificial Intelligence: Volume 1831), D. McAllester (ed.), Berlin: Springer-Verlag, pp. 1-6. (Scholar)
–––, 2006, “Verification: Industrial Applications”, Proof Technology and Computation, H. Schwichtenberg and K. Spies (eds.), Amsterdam: IOS Press, pp. 161–205. (Scholar)
–––, 2009, “Formalizing an Analytic Proof of the Prime Number Theorem”, Journal of Automated Reasoning (Special Issue: A Festschrift for Michael J. C. Gordon), 43 (3): 243–261. (Scholar)
Harrison, J. and L. Théry, 1998, “A Skeptic’s Approach to Combining HOL and Maple”, Journal of Automated Reasoning, 21: 279–294. (Scholar)
Herbrand, J., 1930, Recherches sur la Theorie de la Demonstration, Travaux de la Societé des Sciences at des Lettres de Varsovie, Classe III, Science Mathématique et Physique, No. 33, 128. (Scholar)
Heule, M. J. H. and O. Kullmann, 2017, “The Science of Brute Force”, Communications of the ACM, 60 (8): 70–79. (Scholar)
Heule, M. J. H., O. Kullmann and V. W. Marek, 2016, “Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer”, Theory and Applications of Satisfiability Testing — SAT 2016, 19th International Conference, LNCS 9710, N. Creignou and D. Le Berre (eds.), pp. 228–245. (Scholar)
Hilbert, D. and W. Ackermann, 1928, Principles of Mathematical Logic, L. Hammond, G. Leckie, and F. Steinhardt (trans.), New York: Chelsea Publishing Co., 1950. (Scholar)
Huet, G. P., 1975, “A Unification Algorithm for Typed \(\lambda\)-calculus”, Theoretical Computer Science, 1: 27–57. (Scholar)
Kaliszyk, C. and J. Urban, 2014, “Learning-Assisted Automated Reasoning with Flyspeck”, Journal of Automated Reasoning, 53 (2), 173–213. (Scholar)
Kanckos, A., and B. W. Paleo, 2017, “Variants of Gödel’s Ontological Proof in a Natural Deduction Calculus”, Studia Logica, (3): 553–586. (Scholar)
Kerber, M., Kohlhase and V. Sorge, 1998, “Integrating Computer Algebra into Proof Planning”, Journal of Automated Reasoning, 21: 327–355. (Scholar)
Kirchner, D., 2017, “Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL”, Archive of Formal Proofs. Formal proof development. ISSN: 2150–914x. URL: http://isa-afp.org/entries/PLM.html. (Scholar)
–––, 2021, Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL, Ph.D. Dissertation, Fachbereich Mathematik und Informatik, Freie Universität Berlin. (Scholar)
Kirchner, D., C. Benzmüller and E. Zalta, 2019, “Computer Science and Metaphysics: A Cross-Fertilization”, Open Philosophy, 2: 230–251. (Scholar)
–––, 2020, “Mechanizing Principia Logico-Metaphysica in Functional Type Theory", Review of Symbolic Logic, 13 (1): 206–18. (Scholar)
Knuth, D. and P. B. Bendix, 1970, “Simple Word Problems in Universal Algebras”, in Computational Problems in Abstract Algebra, J. Leech (ed.), Oxford, New York: Pergamon Press, pp. 263–297. (Scholar)
Kleene, S. C., 1962, Introduction to Metamathematics, Amsterdam: North-Holland. (Scholar)
Kovács, L. and A. Voronkov, 2013, “First-Order Theorem Proving and VAMPIRE”, CAV 2013: Proceedings of the International Conference on Computer Aided Verification, N. Sharygina and H. Veith (eds.), LNCS 8044, pp. 1–35. (Scholar)
Kowalski, R., 1974, “Predicate Logic as a Programming Language”, Proceedings of the International Federation for Information Processing (Proc. IFIP ’74), Amsterdam: North Holland, pp. 569–574. (Scholar)
Küchlin, W. and C. Sinz, 2000, “Proving Consistency Assertions for Automotive Product Data Management”, Journal of Automated Reasoning (Special Issue: Satisfiability in the Year 2000), I. P. Gent and T. Walsh (eds.), 24 (1–2): 145–163. (Scholar)
Kühlwein, D., T. van Laarhoven, E. Tsivtsivadze, J. Urban and T. Heskes, 2012, “Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics”, Automated Reasoning: 6th International Joint Conference, IJCAR 2012, (Lecture Notes in Computer Science: Volume 7364), B. Gramlich, D. Miller and U. Sattler (eds.), Manchester, UK: Springer-Verlag, pp. 378–392. (Scholar)
Lemmon, E. J., C. A. Meredith, D. Meredith, A. N. Prioir and I. Thomas, 1957, Calculi of Pure Strict Implication, Philosophy Dept., Canterbury University, Christchurch, New Zealand. (Scholar)
Lloyd, J. W., 1984, Foundations of Logic Programming, Berlin: Springer-Verlag. (Scholar)
Loveland, D. W., 1969, “A Simplified Format for the Model Elimination Procedure”, Journal of the Association for Computing Machinery, 16: 349–363. (Scholar)
–––, 1970, “A Linear Format for Resolution”, Proceedings of the IRIA Symposium on Automatic Demonstration, New York: Springer-Verlag, pp. 147-162. (Scholar)
–––, 1978, Automated Theorem Proving: A Logical Basis, Amsterdam: North Holland. (Scholar)
Luckham, D., 1970, “Refinements in Resolution Theory”, Proceedings of the IRIA Symposium on Automatic Demonstration, New York: Springer-Verlag, pp. 163-190. (Scholar)
Maggesi, M., 2018, “A Formalization of Metric Spaces in HOL Light”, Journal of Automated Reasoning, 60 (2): 237–254. (Scholar)
Martin-Löf, P., 1982, “Constructive Mathematics and Computer Programming”, Logic, Methodology and Philosophy of Science (Volume IV), Amsterdam: North-Holland, pp. 153-175. (Scholar)
Massacci, F. and L. Marraro, 2000, “Logical Cryptanalysis: Encoding and Analysis of the U.S. Data Encryption Standard”, Journal of Automated Reasoning (Special Issue: Satisfiability in the Year 2000), I. P. Gent and T. Walsh (eds.), 24 (1–2): 165–203. (Scholar)
McCarthy, J., 1962, “Towards a Mathematical Science of Computation”, International Federation for Information Processing Congress (Munich, 1962), Amsterdam: North Holland, pp. 21–28. (Scholar)
McCharen, J. D., R. A. Overbeek and L. A. Wos, 1976, “Problems and Experiments for and with Automated Theorem-Proving Programs”, IEEE Transactions on Computers 8: 773–782. (Scholar)
McCune, W., 1997, “Solution of the Robbins Problem”, Journal of Automated Reasoning, 19 (3): 263–276. (Scholar)
–––, 2001, MACE 2.0 Reference Manual and Guide, Mathematics and Computer Science Division, ANL/MSC-TM-249, Argonne National Laboratory. (Scholar)
McRobie, M. A., 1991, “Automated Reasoning and Nonclassical Logics: Introduction”, Journal of Automated Reasoning, 7 (4): 447–451. (Scholar)
Meng, J. and L. C. Paulson, 2008, “Translating higher-order clauses to first-order clauses”, Journal of Automated Reasoning, 40 (1): 35–60. (Scholar)
Meredith, C. A. and A. N. Prior, 1964, “Investigations into Implicational S5”, Z. Math. Logik Grundlagen Math., 10:203–220. (Scholar)
Meyer, J.-J. Ch., 2014, “Logics for Intelligent Agents and Multi-Agent Systems”, Handbook of the History of Logic, Volume 9: Computational Logic, J. Siekmann (ed.), pp. 629–658, Elsevier. (Scholar)
Miller, D. and G. Nadathur, 1988, “An Overview of \(\lambda\)Prolog”, Proceedings of the Fifth International Logic Programming Conference — Fifth Symposium in Logic Programming, R. Bowen and R. Kowalski (eds.), Cambridge, MA: MIT Press. (Scholar)
Minker, J., D. Seipel and C. Zaniolo, 2014, “Logic and Databases: A History of Deductive Databases”, Handbook of the History of Logic, Volume 9: Computational Logic, J. Siekmann (ed.), pp. 571–627, Elsevier. (Scholar)
Muzalewski, M., 1993, An Outline of PC Mizar, Fondation Philippe le Hodey, Brussels. (Scholar)
Nipkow, T., L. C. Paulson and M. Wenzel, 2002, “Isabelle/HOL: A Proof Assistant for Higher-Order Logic“, LNCS Vol. 2283, pp. 207–208. (Scholar)
Nivens, A. J., 1974, “A Human-Oriented Logic for Automatic Theorem Proving”, Journal of the Association of Computing Machinery, 21 (4): 606–621. (Scholar)
Oppenheimer, P. and E. Zalta, 2011, “A Computationally-Discovered Simplification of the Ontological Argument”, Australasian Journal of Philosophy, 89 (2): 333–349. (Scholar)
Paulson, L. C., 1990, “Isabelle: The Next 700 Theorem Provers”, Logic and Computer Science, P. Odifreddi (ed.), Academic Press, pp. 361–386. (Scholar)
–––, 1994, Isabelle: A Generic Theorem Prover (Lecture Notes in Computer Science: Volume 828), Berlin: Springer-Verlag. (Scholar)
–––, 2010. “Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers”, PAAR-2010, B. Konev et al. (eds.), pp. 1–10. (Scholar)
Paulson, L. C. and K. Grabczewski, 1996, “Mechanizing Set Theory”, Journal of Automated Reasoning, 17 (3): 291–323. (Scholar)
Pease, A. and G. Sutcliffe, 2007, “First Order Reasoning on a Large Ontology”, Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Volume 257), G. Sutcliffe and J. Urban (eds.), Bremen. (Scholar)
Pelletier, F. J., 1986, “Seventy-Five Problems for Testing Automatic Theorem Provers”, Journal of Automated Reasoning, 2 (2): 191–216. (Scholar)
–––, 1998, “Natural Deduction Theorem Proving in THINKER”, Studia Logica, 60 (1): 3–43. (Scholar)
Pelletier, F. J., G. Sutcliffe and A. P. Hazen, 2017, “Automated Reasoning for the Dialetheic Logic RM3”, Proceedings of the Thirtieth International Florida Artificial Intelligence Research Society Conference, V. Rus and Z. Markov (eds.), pp. 110–115. (Scholar)
Pelletier, F. J., G. Sutcliffe, and C. Suttner, 2002, “The Development of CASC”, AI Communications, 15 (2–3): 79–90. (Scholar)
Peterson, J. G., 1977, The Possible Shortest Single Axiom for EC-Tautologies, Report 105, Department of Mathematics, University of Auckland. (Scholar)
Pollock, J., 1989, “OSCAR: A General Theory of Rationality”, Journal of Experimental & Theoretical Artificial Intelligence, 1 (3): 209–226 (Scholar)
–––, 1995, Cognitive Carpentry, Cambridge, MA: Bradford/MIT Press. (Scholar)
–––, 2006, “Against Optimality: Logical Foundations for Decision-Theoretic Planning in Autonomous Agents”, Computational Intelligence, 22(1): 1–25. (Scholar)
Portoraro, F. D., 1994, “Symlog: Automated Advice in Fitch-style Proof Construction”, CADE-12: Proceedings of the 12th International Conference on Automated Deduction, (Lecture Notes in Artificial Intelligence: Volume 814), A. Bundy (ed.), Berlin: Springer-Verlag, pp. 802-806. (Scholar)
–––, 1998, “Strategic Construction of Fitch-style Proofs”, Studia Logica, 60 (1): 45–66. (Scholar)
Prasad, M., A. Biere and A. Gupta, 2005, “A Survey of Recent Advances in SAT-Based Formal Verification”, International Journal on Software Tools for Technology Transfer, 7 (2): 156–173. (Scholar)
Prawitz, D., 1965, Natural Deduction: A Proof Theoretical Study, Stockholm: Almqvist & Wiksell. (Scholar)
Quaife, A., 1992, Automated Development of Fundamental Mathematical Theories, Kluwer Academic Publishers. (Scholar)
Robinson, J. A., 1965, “A Machine Oriented Logic Based on the Resolution Principle”, Journal of the Association of Computing Machinery, 12: 23–41. (Scholar)
–––, 1965, “Automatic Deduction with Hyper-resolution”, Internat. J. Comput. Math., 1: 227–234. (Scholar)
Robinson, J. A. and A. Voronkov (eds.), 2001, Handbook of Automated Reasoning: Volumes I and II, Cambridge, MA: MIT Press. (Scholar)
Schmitt, P. and I. Tonin, 2007, “Verifying the Mondex Case Study”, Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, IEEE Computer Society, pp. 47–58. (Scholar)
Schulz, S., 2004, “System Abstract: E 0.81”, Proceedings of the 2nd International Joint Conference on Automated Reasoning (Lecture Notes in Artificial Intelligence: Volume 3097), D. Basin and M. Rusinowitch (eds.), Berlin: Springer-Verlag, pp.223-228. (Scholar)
Scott, D., 1972, “Appendix B: Notes in Dana Scott’s Hand”, in Sobel 2004, pp. 145–146. (Scholar)
Sieg, W. and J. Byrnes, 1996, Normal Natural Deduction Proofs (in Classical Logic), Report CMU-PHIL 74, Department of Philosophy, Carnegie-Mellon University. (Scholar)
Slaney, J. K., 1984, “3,088 Varieties: A Solution to the Ackerman Constant Problem”, Journal of Symbolic Logic, 50: 487–501. (Scholar)
Sobel, J. H., 2004, Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press. (Scholar)
Steen, A. and C. Benzmüller, 2021, “Extensional Higher-Order Paramodulation in Leo-III”, Journal of Automated Reasoning, 65 (6): 775–807. (Scholar)
Stickel, M. E., 1992, “A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog”, Theoretical Computer Science, 104: 109–128. (Scholar)
Suppes, P., et al., 1981, “Part I: Interactive Theorem Proving in CAI Courses”, University-Level Computer-Assisted Instruction at Stanford: 1968–1980, P. Suppes (ed.), Institute for the Mathematical Study of the Social Sciences, Stanford University. (Scholar)
Sutcliffe, G., 2017, “The TPTP Problem Library and Associated Infrastructure”, Journal of Automated Reasoning, 59 (4): 483–502. (Scholar)
Sutcliffe, G. and C. Benzmüller, 2010, “Automated Reasoning in Higher-Order Logic Using TPTP THF Infrastructure”, Journal of Formalized Reasoning, 43 (4): 337–362. (Scholar)
Sutcliffe, G. and C. Suttner, 1998, “The TPTP Problem Library – CNF Release v1.2.1”, Journal of Automated Reasoning, 21 (2): 177–203. (Scholar)
Szabo, M. E. (ed.), 1969, The Collected Papers of Gerhard Gentzen, Amsterdam: North-Holland. (Scholar)
Trybulec, A., 1978, “The Mizar Logic Information Language”, Bulletin of the Association for Literary Linguistic Computing, 6(2): 136–140. (Scholar)
Trybulec, A. and H. Blair, 1985, “Computer Assisted Reasoning with Mizar”, Proceedings of the 9th International Joint Conference on Artificial Intelligence, (IJCAI-85: Volume 1), Los Angeles, pp. 26–28. (Scholar)
Turing, A., 1936, “On computable numbers, with an application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society, 42 (2): 230–265. (Scholar)
Urban, J., 2007, “MaLARea: A Metasystem for Automated Reasoning in Large Theories”, Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, J. Urban, G. Sutcliffe and S. Schulz (eds.), pp. 45–58. (Scholar)
Urban, J., K. Hoder, A. Voronkov, 2010, “Evaluation of Automated Theorem Proving on the Mizar Mathematical Library”, Mathematical Software – ICMS 2010: Proceedings of the Third International Congress on Mathematical Software, Kobe, Japan, (Lecture Notes in Computer Science, Volume 6327), pp. 155–166. (Scholar)
Urban, J. and J. Vyskocil, 2012, “Theorem Proving in Large Formal Mathematics as an Emerging AI Field”, arXiv:1209.3914 [cs.AI], Report No. DPA-12271, Cornell University. (Scholar)
Urquhart, A., 1987, “Hard Examples for Resolution”, Journal of the ACM, 34 (1): 209–219. (Scholar)
–––, 1994 (ed.), The Collected Papers of Bertrand Russell, Volume 4: Foundations of Logic, 1903-05, Routledge, London and New York.
van Benthem Jutting, L. S., 1977, Checking Landau’s “Grundlagen” in the Automath system, Ph.D. Thesis, Eindhoven University of Technology; published in Mathematical Centre Tracts, Number 83, Amsterdam: Mathematisch Centrum, 1979. (Scholar)
Voronkov, A., 1995, “The Anatomy of Vampire: Implementing Bottom-Up Procedures with Code Trees”, Journal of Automated Reasoning, 15 (2): 237–265. (Scholar)
Wallen, L. A., 1990, Automated Deduction in Nonclassical Logics, Cambridge, MA: MIT Press. (Scholar)
Wang, H., 1960, “Proving Theorems by Pattern Recognition – I”, in Automation of Reasoning (Volume 1), J. Siekmann and G. Wrightson (eds.), Berlin: Springer-Verlag, 1983, pp. 229–243. (Scholar)
–––, 1960, “Toward Mechanical Mathematics”, in Automation of Reasoning (Volume 1), J. Siekmann and G. Wrightson (eds.), Berlin: Springer-Verlag, 1983, pp. 244-264. (Scholar)
Wegner, B., 2011, “Completeness of reference databases, old-fashioned or not?”, Newsletter of the European Mathematical Society, 80: 50–52. (Scholar)
Wiedijk, F., 2006, The Seventeen Provers of the World, (Lecture Notes in Artificial Intelligence: Volume 3600), F. Wiedijk (ed.), New York: Springer-Verlag. (Scholar)
–––, 2007, “The QED Manifesto Revisited”, Studies in Logic, Grammar and Rhetoric, 10 (23): 121–133. (Scholar)
Wooters, W.K. and W. H. Zurek, 1982, “A single quantum cannot be cloned”, Nature, 299: 802–803.
Wos, L. (ed.), 2001, Journal of Automated Reasoning (Special Issue: Advances in Logic Through Automated Reasoning), 27 (2). (Scholar)
Wos, L., D. Carson and G. R. Robinson, 1965, “Efficiency and Completeness of the Set of Support Strategy in Theorem Proving”, Journal of the Association of Computing Machinery, 12: 698–709. (Scholar)
Wos, L., R. Overbeek, E. Lusk and J. Boyle, 1984, Automated Reasoning: Introduction and Applications, Englewood Cliffs, NJ: Prentice-Hall. (Scholar)
Wos, L., D. Ulrich, and B. Fitelson, 2002, “Vanquishing the XCB Question; The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus”, Journal of Automated Reasoning, 29 (2):107–124. (Scholar)
Wos, L., S. Winker, R. Veroff, B. Smith and L. Henschen, 1983, “Questions Concerning Possible Shortest Single Axiom for the Equivalential Calculus: An Application of Automated Theorem Proving to Infinite Domains”, Notre Dame Journal of Formal Logic, 24: 205–223. (Scholar)
Yoo, J., E. Jee and S. Cha, 2009, “Formal Modeling and Verification of Safety-Critical Software”, IEEE Software, 26 (3): 42–49. (Scholar)
Zalta, E., 1983, Abstract Objects: An Introduction to Axiomatic Metaphysics, Synthese Library, SYLI Volume 160, Springer. (Scholar)
–––, 1999, “Natural Numbers and Natural Cardinals as Abstract Objects: A Partial Reconstruction of Frege’s Grundgesetze in Object Theory”, Journal of Philosophical Logic, 28 (6): 619–660. (Scholar)
–––, 2018, “How Computational Investigations Improved an Ontology”, 2018 Annual Meeting of the International Association for Computing and Philosophy, Warsaw, Polska Akademia Nauk (PAN), Copernicus Center, (Scholar)
–––, 2022, Principia Logico-Metaphysica, Draft/Excerpt dated September 2, 2022, URL: http://mally.stanford.edu/principia.pdf (Scholar)
Zhang, L. and S. Malik, 2002, “The Quest for Efficient Boolean Satisfiability Solvers”, CADE-18: Proceedings of the 18th International Conference on Automated Deduction, (Lecture Notes in Artificial Intelligence: Volume 2392), A. Voronkov (ed.), Berlin: Springer-Verlag, pp. 295-313. (Scholar)

Generated Mon Sep 9 23:41:18 2024

Applied ethics	Epistemology	History of Western Philosophy	Meta-ethics	Metaphysics	Normative ethics
Philosophy of biology	Philosophy of language	Philosophy of mind	Philosophy of religion	Science Logic and Mathematics	More ...