Alberti F., Armando A., Ranise S. (2011), An Automated Symbolic Analysis of Security Policies, Bj{\o}rner N., Sofronie-Stokkermans V., Proceedings of the 23rd International Conference on Automated Deduction (Wroclaw, Poland), 26-33, Lecture Notes in Artificial Intelligence 6803, Springer-Verlag.
Alberti F., Armando A., Ranise S. (2011), Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-Policies, Sandhu R., Wong D., Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security (Hong Kong), 165-175, ACM Press.
Alechina N., Mendler M., de Paiva V., Ritter E. (2001), Categorical and Kripke Semantics for Constructive S4 Modal Logic, Fribourg L., Proceedings of the 15th International Workshop on Computer Science Logic (Paris, France), 292-307, Lecture Notes in Computer Science 2142, Springer-Verlag.
Alexander Steen (2022), An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning (Short Paper), Konev B., Schon C., Steen A., Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning (Haifa, Israel), Online, CEUR Workshop Proceedings 3201.
Alexander G. (1995), Proving First-Order Equality Theorems with Hyper-Linking, PhD thesis, University of North Carolina at Chapel Hill (Chapel Hill, USA).
Allen J.F., Kautz H.A., Pelavin R.N., Tenenberg J.D. (1991), Reasoning about Plans, Morgan Kaufmann Publishers.
Alvez J., Gonzalez-Dios I., Rigau G. (2018), Cross-checking WordNet and SUMO Using Meronymy, Calzolari N., Choukri K., Cieri C., Declerck T., Goggi S., Hasida K., Isahara H., Maegaard B., Mariani J., Mazo H., Moreno A., Odijk J., Piperidis S., Tokunaga T., Proceedings of the 11th Language Resources and Evaluation Conference (Miyazaki, Japan).
Alvez J., Lucio P., Rigau G. (2012), Adimen-SUMO: Reengineering an Ontology for First-Order Reasoning, International Journal on Semantic Web and Information Systems 8(3), 80-116, IGI Global.
American Mathematical Society (1992), Mathematical Subject Classification, S1-S35, American Mathematical Society.
Anantharaman S., Bonacina M.P. (1990), An Application of the Theorem Prover SBR3 to Many-Valued Logic, Okada M., Kaplan S., Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada), 156-161, Lecture Notes in Computer Science 516, Springer-Verlag.
Anantharaman S., Hsiang J. (1990), Automated Proofs of the Moufang Identities in Alternative Rings, Journal of Automated Reasoning 6(1), 79-110.
Andrews P.B. (1989), On Connections and Higher-Order Logic, Journal of Automated Reasoning 5(3), 257-291.
Andrews P.B. (1986), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press.
Andrews P.B. (1972), General Models and Extensionality, Journal of Symbolic Logic 37(2), 395-397.
Andrews P.B. (1971), Resolution in Type Theory, Journal of Symbolic Logic 36(3), 414-432.
Angshuman G., Zhang H. (1989), Andrews' Challenge Problem: Clause Conversion and Solutions, AAR Newsletter 14, 5-8.
Argonne National Laboratory, The Argonne National Laboratory Problem Collection, Previously available from http://info.mcs.anl.gov/.
Arkoudas K., Bringsjord S., Bello P. (2006), Toward Ethical Robots via Mechanized Deontic Logic, Anderson M., Anderson S.L., Armen C., Machine Ethics: Papers from the 2005 AAAI Fall Symposium (Arlington, USA), 17-23, Technical Report FS-05-06, AAAI Press.
Armando A., Bonacina M., Ranise S., Schulz S. (2009), New Results on Rewrite-based Satisfiability Procedures, ACM Transactions on Computational Logic 10(1:4).
Armando A., Ranise S. (2010), Automated Symbolic Analysis of ARBAC Policies, Cuellar J., Lopez J., Proceedings of the 6th International Workshop on Security and Trust Management (Athens, Greece), Springer-Verlag.
Arthan R., Oliva P. (2013), Dual Hoops Have Unique Halving, Bonacina M.P., Stickel M., Automated Reasoning and Mathematics: Essays in Memory of William McCune, To appear, Lecture Notes in Artificial Intelligence, Springer-Verlag.
Aschbacher M., Kinyon M., Phillips J.D. (2006), Finite Bruck Loops, Transactions of the American Mathematical Society 358, 3061-3075.
Astrachan O.L. (1992), METEOR: Exploring Model Elimination Theorem Proving, CS-1992-22, Department of Computer Science, Duke University (Durham, USA).
Avenhaus J., Denzinger J., Fuchs M. (1995), DISCOUNT: A System for Distributed Equational Deduction, Hsiang J., Proceedings of the 6th International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany), 397-402, Springer-Verlag.
Avigad J., Dean E., Mumma J. (2008), A Formal System for Euclid's Elements, arXiv:0810.4315v3.
Baader F., Nipkow T. (1999), Term Rewriting and All That, Cambridge University Press.
Baaz M., Hetzl S., Leitsch A., Richter C., Spohr H. (2008), CERES: An Analysis of Fürstenberg's Proof of the Infinity of Primes, Theoretical Computer Science.
Bachmair L., Dershowitz N. (1986), Commutation, Transformation, and Termination, Siekmann J., Proceedings of the 8th International Conference on Automated Deduction (Oxford, United Kingdom), 5-20, Lecture Notes in Computer Science 230, Springer-Verlag.
Back R. (1989), A Method for Refining Atomicity in Parallel Algorithms, Odijk E., Rem M., Syr J., Proceedings of Parallel Architectures and Languages Europe (Eindhoven, Netherlands), 199-216, Lecture Notes in Computer Science 366, Springer-Verlag.
Back R., von Wright J. (998), Refinement Calculus: A Systematic Introduction, Graduate Texts in Computer Science, Springer-Verlag.
Backes J. (2010), Tableaux for Higher-Order Logic with If-Then-Else, Description and Choice, MSc thesis, Saarland University (Saarbruecken, Germany).
Bailin S., Barker-Plummer D. (1993), L-match: An Inference Rule for Incrementally Elaborating Set Instantiations, Journal of Automated Reasoning 11(3), 391-428.
Baldoni M. (1998), Normal Multimodal Logics: Automatic Deduction and Logic Programming Extensions, PhD thesis, Universita degli studi di Torino (Torino, Italy).
Balsiger P., Heuerding A., Schwendimann S. (2000), A Benchmark Method for the Propositional Modal Logics K, KT, S4, Journal of Automated Reasoning 24(3), 297-317.
Bancerek G. (2001), Duality Based on the Galois Connection. Part I, Journal of Formalized Mathematics 9(4), 767-778.
Bancerek G. (1997), Bounds in Posets and Relational Substructures, Journal of Formalized Mathematics 6(1), 81-91.
Bancerek G. (1997), Directed Sets, Nets, Ideals, Filters, and Maps, Journal of Formalized Mathematics 6(1), 93-107.
Bancerek G. (1997), Prime Ideals and Filters, Journal of Formalized Mathematics 6(2), 241-247.
Bancerek G. (1996), Ideals, Journal of Formalized Mathematics 5(2), 149-156.
Bancerek G. (1991), Complete Lattices, Journal of Formalized Mathematics 2(5), 719-725.
Bancerek G. (1991), Filters - Part II. Quotient Lattices Modulo Filters and Direct Product of Two Lattices, Journal of Formalized Mathematics 2(3), 433-438.
Bancerek G. (1990), The Ordinal Numbers, Journal of Formalized Mathematics 1(1), 91-96.
Bancerek G. (1990), The Well Ordering Relations, Journal of Formalized Mathematics 1(1), 123-129.
Bancerek G. (1990), Zermelo Theorem and Axiom of Choice, Journal of Formalized Mathematics 1(2), 265-267.
Bancerek G., Endou N. (2001), Compactness of Lim-inf Topology, Journal of Formalized Mathematics 9(4), 739-743.
Bancerek G., Endou N., Sakai Y. (2001), On the Characterizations of Compactness, Journal of Formalized Mathematics 9(4), 733-738.
Barcan R. (1946), A Functional Calculus of First Order Based on Strict Implication, Journal of Symbolic Logic 11, 1-16.
Barendregt H.P. (1981), The Lambda Calculus: Its Syntax and Semantics, North-Holland.
Barker-Plummer D (1992), Gazing: An Approach to the Problem of Definition and Lemma Use, Journal of Automated Reasoning 8(3), 311-344.
Baumgartner P. (2015), SMTtoTPTP - A Converter for Theorem Proving Formats, Felty A., Middeldorp A., Proceedings of the 25th International Conference on Automated Deduction (Berlin, Germany), 285-294, Lecture Notes in Computer Science 9195, Springer-Verlag.
Baumgartner P. (1999), FTP'2000 - Problem Sets, ftp://ftphost.uni-koblenz.de/outgoing/agki/FTP2000/ProblemSets/index.html.
Baumgartner P. (1996), Linear and Unit-Resulting Refutations for Horn Theories, Journal of Automated Reasoning 16(3), 241-319.
Baumgartner P. (1994), Refinements of Theory Model Elimination and a Variant without Contrapositives, Cohn A.G., Proceedings of the 11th European Conference on Artificial Intelligence, 90-94, Wiley and Sons.
Baumgartner P., Bax J. (2013), Proving Infinite Satisfiability, McMillan K., Middeldorp A., Voronkov A., Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Stellenbosch, South Africa), 86-95, Lecture Notes in Computer Science 8312, Springer-Verlag.
Baumgartner P., Furbach U. (1994), PROTEIN: A PROver with a Theory Extension INterface, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 769-773, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.
Baumgartner P., Furbach U. (1994), Model Elimination without Contrapositives and its Application to PTTP, Journal of Automated Reasoning 13(3), 339-359.
Baumgartner P., Furbach U., Stolzenburg F. (1997), Computing Answers with Model Elimination, Artificial Intelligence 90, 135-176.
Baumgartner P., Furbach U., Stolzenburg F. (1995), Model Elimination, Logic Programming and Computing Answers, Mellish C.S., Proceedings of the 14th International Joint Conference on Artificial Intelligence, 335-340, Morgan Kaufmann.
Baumgartner P., Slaney J. (2009), Constraint Modelling: A Challenge for Automated Reasoning, Peltier N., Sofronie-Stokkermans V., Proceedings of the 7th International Workshop on First-Order Theorem Proving (Oslo, Norway), 4-18, CEUR Workshop Proceedings 556.
Beckert B., Hahnle R., Schmitt P. (2007), Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science 4334, Springer-Verlag.
Beckert B., Posegga J. (1995), leanTAP: Lean, Tableau-based Deduction, Journal of Automated Reasoning 15(3), 339-358.
Beeson M., Wos L. (2017), Finding Proofs in Tarskian Geometry, Journal of Automated Reasoning 58(1), 181-207.
Belinfante J.G.F. (1997), On Quaife's Development of Class Theory, AAR Newsletter 37, 1-4.
Benanav D. (1992), Recognising Unnecessary Clauses in Resolution Based Systems, Journal of Automated Reasoning 9(1), 43-76.
Bennett F.E. (1989), Quasigroup Identities and Mendelsohn Designs, Canadian Journal of Mathematics 41(2), 341-368.
Bennett F.E., Zhu L. (1992), Conjugate-Orthogonal Latin Squares and Related Structures, Dinitz J.H., Douglas R.S., Contemporary Design Theory: A Collection of Surveys, 41-96, Wiley and Sons.
Bentkamp A., Blanchette J., Tourret S., Vukmirovi{\'c} P., Waldmann U. (2019), Superposition with Lambdas, Fontaine P., Proceedings of the 27th International Conference on Automated Deduction (Natal, Brazil), 55-73, Lecture Notes in Computer Science 11716, Springer-Verlag.
Benzmüller C. (2023), A Simplified Variant of Gödel's Ontological Argument, Vestrucci A., Beyond Babel: Religions in a Linguistic Pluralism, To appear, Sophia Studies in Cross-Cultural Philosophy of Traditions and Cultures, Springer.
Benzmüller C. (2011), Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics Theory, Annals of Mathematics and Artificial Intelligence, Springer-Verlag.
Benzmüller C. (2010), Simple Type Theory as a Framework for Combining Logics, Proceedings of the 3rd World Congress and School on Universal Logic (Lisbon, Portugal), To appear.
Benzmüller C. (2008), Automating Access Control Logics in Simple Type Theory with LEO-II, SEKI Technical Report SR-2008-01, Universität des Saarlandes (Saarbrücken, Germany).
Benzmüller C. (1999), Equality and Extensionality in Higher-Order Theorem Proving, PhD thesis, Department of Computer Science, Saarland University (Saarbruecken, Germany).
Benzmüller C., Brown C.E. (2007), The Curious Inference of Boolos in MIZAR and OMEGA, Matuszewski R., Zalewska A., Studies in Logic, Grammar, and Rhetoric 10(23), Festschrift in Honour of Andrzej Trybulec, 299-388.
Benzmüller C., Brown C.E. (2005), A Structured Set of Higher-Order Problems, Hurd J., Melham T., Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (Oxford, United Kingdom), 66-81, Lecture Notes in Artificial Intelligence 3606, Springer-Verlag.
Benzmüller C., Cheikhrouhou L., Fehrer D., Fiedler A., Huang X., Kerber M., Kohlhase M., Konrad K., Meier A., Melis E., Schaarschmidt W., Siekmann J., Sorge V. (1997), OMEGA: Towards a Mathematical Assistant, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 252-255, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.
Benzmüller C., Paulson L. (2013), Quantified Multimodal Logics in Simple Type Theory, Logica Universalis 7(1), 7-20, Springer-Verlag.
Benzmüller C., Paulson L. (2010), Multimodal and Intuitionistic Logics in Simple Type Theory, Logic Journal of the IGPL, Oxford University Press.
Benzmüller C., Paulson L. (2008), Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II, Benzmüller C., Brown C.E., Siekmann J., Statman R., Reasoning in Simple Type Theory: Festschrift in Honour of Peter B. Andrews on his 70th Birthday, 401-422, Studies in Logic, Mathematical Logic and Foundations 17, College Publications.
Benzmüller C., Pease A. (2010), Progress in Automating Higher-order Ontology Reasoning, Proceedings of IJACR 2010 Workshop on Practical Aspects of Automated Reasoning (Edinburgh, United Kingdom).
Benzmüller C., Sorge V., Jamnik M., Kerber M. (2008), Combined Reasoning by Automated Cooperation, Journal of Applied Logic 6(3), 318-342.
Benzmüller C., Sorge V., Jamnik M., Kerber M. (2005), Can a Higher-Order and a First-Order Theorem Prover Cooperate?, Baader F., Voronkov A., Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Montevideo, Uruguay), 415-431, Lecture Notes in Artificial Intelligence 3452, Springer-Verlag.
Berdine J., Calcagno C., O'Hearn P. (2006), Smallfoot: Modular Automatic Assertion Checking with Separation Logic, de Boer F., Bonsangue M., Graf S., de Roever W-P., Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (Amsterdam, The Netherlands), 115-137, Lecture Notes in Computer Science 4111, Springer-Verlag.
Berdine J., Calcagno C., O'Hearn P. (2005), Symbolic Execution with Separation Logic, Yi K., Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (Tsukuba, Japan), 52-68, Lecture Notes in Computer Science 3780, Springer-Verlag.
Bhayat A., Reger G. (2020), A Polymorphic Vampire, Peltier N., Sofronie-Stokkermans V., Proceedings of the 10th International Joint Conference on Automated Reasoning (Online), 361–368, Lecture Notes in Artificial Intelligence 12167.
Birkhoff G., Bartee T. (1970), Modern Applied Algebra, McGraw-Hill.
Birkhoff G., MacLane S. (1965), A Survey of Modern Algebra, Macmillan.
Bishop R., Goldberg S. (1980), Tensor Analysis on Manifolds, Dover.
Blackburn P., van Benthem J., Wolther F. (2006), Handbook of Modal Logic, Studies in Logic and Practical Reasoning 3, Elsevier Science.
Blanchette J. (2015), The Editor's Corner, AAR Newsletter 112, http://www.aarinc.org/Newsletters/112-2015-09.html.
Blanchette J. (2009), Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm, Journal of Automated Reasoning 43(1), 1-18.
Blanchette J. (2008), The Textbook Proof of Huffman's Algorithm, Archive of Formal Proofs, http://isa-afp.org/entries/Huffman.shtml.
Blanchette J., Boehme S., Paulson L. (2011), Extending Sledgehammer with SMT Solvers, Bj{\o}rner N., Sofronie-Stokkermans V., Proceedings of the 23rd International Conference on Automated Deduction (Wroclaw, Poland), 116-130, Lecture Notes in Artificial Intelligence 6803, Springer-Verlag.
Blanchette J., Haslbeck M., Matichuk D., Nipkow T. (2015), Mining the Archive of Formal Proofs, Kerber M., Carette J., Kaliszyk C., Rabe F., Sorge V., Proceedings of the 8th Conference on Intelligent Computer Mathematics (Washington, USA), 3-17, Lecture Notes in Computer Science 9150.
Blanchette J., Hölzl J., Lochbihler A., Panny L., Popescu A., Traytel D. (2014), Truly Modular (Co)datatypes for Isabelle/HOL, Klein G., Gamboa R., Proceedings of the 5th International Conference on Interactive Theorem Proving (Vienna, Austria), 93-110, Lecture Notes in Computer Science 8558, Springer-Verlag.
Blanchette J., Popescu A., Traytel D. (2014), Abstract Completeness, Archive of Formal Proofs, http://isa-afp.org/entries/Abstract_Completeness.shtml.
Bledsoe W.W. (1990), Challenge Problems in Elementary Calculus, Journal of Automated Reasoning 6(3), 341-359.
Bledsoe W.W. (1977), Non-resolution Theorem Proving, Artificial Intelligence 9, 1-35.
Bledsoe W.W., Boyer R.S., Henneman W.H. (1972), Computer Proofs of Limit Theorems, Artificial Intelligence 3, 27-60.
Bledsoe W.W., Feng G. (1993), SET-VAR, Journal of Automated Reasoning 11(3), 293-314.
Blyth I.S., Varlet I.C. (1994), Ockham Algebras, Oxford Science Publications.
Bobot F., Filliatre J-C., Marche C., Melquiond G., Paskevich A. (2014), Toccata: Certified Programs and Certified Tools, http://toccata.lri.fr/gallery/why3.en.html.
Bock C., Gruninger M. (2005), PSL: A Semantic Domain for Flow Models, Journal of Software and Systems Modeling 4(2), 209-231.
Boeva V., Ekenberg L. (2004), A Transition Logic for Schemata Conflicts, Data and Knowledge Engineering 51(3), 277-294.
Bonacina M.P. (1991), Problems in \Lukasiewicz Logic, AAR Newsletter 18, 5-12.
Bond M., Anderson R. (2001), API-Level Attacks on Embedded Systems, Computer 34(10), 67-75.
Boolos G. (1987), A Curious Inference, Journal of Philosophical Logic 16, 1-12.
Boolos G., Burgess J., Jeffrey R. (2003), Computability and Logic, Cambridge University Press.
Bourbaki N. (1989), Algebra I - Chapters 1-3, Springer Verlag.
Bourely C., Caferra R., Peltier N. (1994), A Method for Building Models Automatically. Experiments with an Extension of Otter, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 72-86, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.
Boyer R., Lusk E.L., McCune W.W., Overbeek R., Stickel M.E., Wos L. (1986), Set Theory in First-Order Logic: Clauses for Godel's Axioms, Journal of Automated Reasoning 2(3), 287-327.
Boyer R., Moore J. (1988), Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, Machine Intelligence 11, 83-124.
Bretier P., Sadek M. (1996), Rational Agent as the Kernel of a Cooperative Spoken Dialogue System: Implementing a Logical Theory of Interaction, Müller J., Wooldridge M., Jennings N., Proceedings of the 3rd Workshop on Intelligent Agents - Agent Theories, Architectures, and Languages (Budapest, Hungary), 189-203, Lecture Notes in Computer Science 1193, Springer-Verlag.
Bronsard F., Reddy U., Hasker R. (1996), Induction using Term Orders, Journal of Automated Reasoning 16(1-2), 3-37.
Brown C. (2024), Simple Difficult Problems for Automated Theorem Provers, Czech Tecnical University in Prague.
Brown C., Gauthier T., Kaliszyk C., Sutcliffe G., Urban J. (2019), GRUNGE: A Grand Unified ATP Challenge, Fontaine P., Proceedings of the 27th International Conference on Automated Deduction (Natal, Brazil), 123-141, Lecture Notes in Computer Science 11716, Springer-Verlag.
Brown C.E. (2011), Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems, Bj{\o}rner N., Sofronie-Stokkermans V., Proceedings of the 23rd International Conference on Automated Deduction (Wroclaw, Poland), 147-161, Lecture Notes in Artificial Intelligence 6803, Springer-Verlag.
Brown C.E. (2008), M-Set Models, Benzmüller C., Brown C.E., Siekmann J., Statman R., Reasoning in Simple Type Theory: Festschrift in Honour of Peter B. Andrews on his 70th Birthday, 175-186, Studies in Logic, Mathematical Logic and Foundations 17, College Publications.
Brown C.E., Smolka G. (2009), Terminating Tableaux for the Basic Fragment of Simple Type Theory, Giese M., Waaler A., Proceedings of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Oslo, Norway), 138-151, Lecture Notes in Artificial Intelligence 5697, Springer-Verlag.
Brown C.E., Smolka G. (2009), Extended First-Order Logic, Nipkow T., Urban C., Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (Munich, Germany), 164-179, Lecture Notes in Computer Science 5674, Springer-Verlag.
Brushi M. (1991), The Halting Problem, AAR Newsletter 17, 7-12.
Buch A., Hillenbrand T. (1996), Waldmeister: Development of a High Performance Completion-based Theorem Prover, SEKI-Report SR-96-01, AG Effiziente Algorithmen, Universität Kaiserslautern (Kaiserslautern, Germany).
Buch A., Hillenbrand T., Fettig R. (1996), Waldmeister: High Performance Equational Theorem Proving, Calmet J., Limongelli C., Proceedings of the International Symposium on Design and Implementation of Symbolic Computation Systems (Karlsruhe, Germany), 63-64, Lecture Notes in Computer Science 1128, Springer-Verlag.
Bull J., Otway D.J. (1997), The Authentication Protocol, DRA/CIS3/PROJ/CORBA/SC/1/CSM/436-04/03, Defence Research Agency.
Bumcroft R. (1965), , Proceedings of the Glasgow Mathematical Association 7(1).
Bundy A. (1999), The Advantages of Binary Sinks, Blue Book Note 1311, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Bundy A. (1997), Non-structural Inductions and Rippling, Blue Book Note 1188, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Bundy A. (1995), Rippling in Harald's Problem, Blue Book Note 978, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Bundy A. (1994), Shankar's Arithmetic/Geometic Mean Proof, Blue Book Note 951, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Bundy A. (1992), How to Prove Pete's Nasty Theorem, Blue Book Note 725, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Bundy A. (1989), An Analysis of the Arithmetic/Geometric Mean Theorem, Blue Book Note 524, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Bundy A. (1983), The Computer Modelling of Mathematical Reasoning, Academic Press.
Burkholder L. (1987), A 76th Automated Theorem Proving Problem, AAR Newsletter 8, 6-7.
Burkholder L. (1987), The Halting Problem, SIGCSE bulletin.
Burrows M., Abadi M., Needham R. (1989), A Logic of Authentication, Proceedings of the Royal Society 426(1871).
Bylinski C. (1990), Functions and Their Basic Properties, Journal of Formalized Mathematics 1(1), 55-65.
Bylinski C. (1990), Some Basic Properties of Sets, Journal of Formalized Mathematics 1(1), 47-53.
Byli{\'n}ski C. (1990), Functions from a Set to a Set, Journal of Formalized Mathematics 1(1), 153-164.
Böhme S., Nipkow T. (2010), Sledgehammer: Judgement Day, Giesl J., Haehnle R., Proceedings of the 5th International Joint Conference on Automated Reasoning (Edinburgh, United Kingdom), 107-121, Lecture Notes in Artificial Intelligence 6173.
Börger E., Grädel E., Gurevich Y. (2001), The Classical Decision Problem, 33, Springer-Verlag.
Calvanese D., De Giacomo G., Lembo D., Lenzerini M., Rosati R. (2007), EQL-Lite: Effective First-Order Query Processing in Description Logics, Velosco M., Proceedings of the 20th International Joint Conference on Artificial Intelligence (Hyderabad, India), 274-279.
Caminati M., Kerber M., Lange C., Rowat C. (2015), Sound Auction Specification and Implementation, Feldman M., Schwarz M., Roughgarden T., Proceedings of the 16th ACM Conference on Economics and Computation (Portland, USA), 547-564, ACM Press.
Carroll G.R., Hannan M.T. (2000), The Demography of Corporations and Industries, Princeton University Press.
Carroll L. (1986), Lewis Carroll's Symbolic Logic, C.N. Potter.
Cerna D. (2015), Advances in Schematic Cut Elimination, PhD thesis, Technical University of Vienna.
Cerna D., Leitsch A. (2016), Schematic Cut Elimination and the Ordered Pigeonhole Principle, Olivetti N., Tiwari A., Proceedings of the 8th International Joint Conference on Automated Reasoning (Coimbra, Portugal), 241-256, Lecture Notes in Artificial Intelligence 9706.
Chang C-L. (1970), The Unit Proof and the Input Proof in Theorem Proving, Journal of the ACM 17(4), 698-707.
Chang C-L., Lee R.C-T. (1973), Symbolic Logic and Mechanical Theorem Proving, Academic Press.
Chaudhri V., Elenius D., Goldenkranz A., Gong A., Martone M., Webb W., Yorke-Smith N. (2014), Comparative Analysis of Knowledge Representation and Reasoning Requirements Across a Range of Life Sciences Textbooks, Journal of Biomedical Semantics 5(51).
Chaudri V., Cheng B., Overholtzer A., Roschelle J., Spaulding A., Clark P., Greaves M., Gunning D. (2013), Inquire Biology: A Textbook that Answers Questions, AI Magazine 34(3).
Chaudri V., Dinesh N., Inclezan D. (2013), Three Lessons in Creating a Knowledge Base to Enable Explanation, Reasoning and Dialog, Klenk M., Laird J., Proceedings of the 2nd Annual Conference on Advances in Cognitive Systems (Baltimore, USA), 187-203.
Chellas B.F. (1980), Modal Logic, Cambridge University Press.
Chou S., Gao X., Zhang J. (2000), A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering, Journal of Automated Reasoning 25(3), 219-246.
Chu H., Plaisted D. (1994), Semantically Guided First-order Theorem Proving using Hyper-linking, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 192-206, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.
Church A. (1956), Introduction to Mathematical Logic I, Princeton University Press.
Claessen K., Hähnle R., M{\aa}rtensson J. (2002), Verification of Hardware Systems with First-Order Logic, Sutcliffe G., Pelletier J., Suttner C., Proceedings of the CADE-18 Workshop - Problem and Problem Sets for ATP (Copenhagen, Denmark), Department of Computer Science, University of Copenhagen, Technical Report 02/10.
Claessen K., Lilliestrom A. (2009), Automated Inference of Finite Unsatisfiability, Schmidt R., Proceedings of the 22nd International Conference on Automated Deduction (Montreal Canada), 388-403, Lecture Notes in Artificial Intelligence 5663, Springer-Verlag.
Claessen K., Smallbone N. (2018), Efficient Encodings of First-Order Horn Formulas in Equational Logic, Galmiche D., Schulz S., Sebastiani R., Proceedings of the 9th International Joint Conference on Automated Reasoning (Oxford, United Kingdom), 388-404, Lecture Notes in Computer Science 10900.
Cohen E. (2000), Separation and Reduction, Backhouse R., Oliveira J., Proceedings of the 5th International Conference on the Mathematics of Program Construction (Ponte de Lima, Portugal), 45-59, Lecture Notes in Computer Science 1837.
Cok D., Stump A., Weber T. (2015), The 2013 Evaluation of SMT-COMP and SMT-LIB, Journal of Automated Reasoning 55(1), 61-90.
Comaromi J.P., Beall J., Matthews W.E., New G.R. (1989), Dewey Decimal Classification and Relative Index, Forest Press.
Conway J. (1971), Regular Algebra and Finite Machines, Chapman and Hall.
Cook S., Reckhow R. (1979), The Relative Efficiency of Propositional Proof Systems, Journal of Symbolic Logic 44, 36-50.
Cramer M., Fisseni B., Koepke P., Kühlwein D., Schröder B., Veldman J. (2010), The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts, Fuchs N., Proceedings of the Workshop on Controlled Natural Languages (Marettimo Island, Italy), Lecture Notes in Artificial Intelligence 5972, Springer-Verlag.
Csörgö P., Dr{\'a}pal A., Kinyon M. (2010), Buchsteiner Loops, International Journal of Algebra and Computation 19(8), 1049-1088.
Curry H.B., Feys R. (1958), Combinatory Logic I, North Holland, Amsterdam.
Curry H.B., Hindley J.R., Seldin J.P. (1972), Combinatory Logic II, North Holland, Amsterdam.
Darmochwa{\l} A. (1990), Compact Spaces, Journal of Formalized Mathematics 1(2), 383-386.
Darmochwa{\l} A. (1989), Finite Sets, Journal of Formalized Mathematics 1(1), 165-167.
de Melo G., Suchanek F., Pease A. (2008), Integrating YAGO into the Suggested Upper Merged Ontology, Chung S., Proceedings of the 20th IEEE International Conference on Tools with Artificial Intelligence (Dayton, USA), 190-193, IEEE Computer Society.
de Nivelle H. (), Bliksem Resolution Prover, http://www.ii.uni.wroc.pl/~nivelle/software/bliksem.
de Nivelle H. (2011), Classical Logic with Partial Functions, Journal of Automated Reasoning 47(4), 399-425.
de Nivelle H. (2010), Classical Logic with Partial Functions, Giesl J., Haehnle R., Proceedings of the 5th International Joint Conference on Automated Reasoning (Edinburgh, United Kingdom), 203-217, Lecture Notes in Artificial Intelligence 6173.
de Nivelle H., Piskac R. (2005), Verification of an Off-Line Checker for Priority Queues, Aichernig B., Beckert B., Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (Los Alamitos, USA), 210-219.
DeChampeaux D. (1979), Sub-problem Finder and Instance Checker: Two Co-operating Preprocessors for Theorem Provers, Proceedings of the 6th International Joint Conference on Artificial Intelligence, 191-196, Morgan Kaufmann.
DeChampeaux D. (1972), Sub-problem Finder and Instance Checker: Two Co-operating Preprocessors for Theorem Provers, Journal of the ACM 33, 633-657.
Deharbe D. (2022), Proof Obligations from the B Formal Method (Version 20220905), Zenodo, DOI: 10.5281/zenodo.7050797.
Delaune S., Kremer S., Steel G. (2008), Formal Analysis of PKCS#11, Sabelfeld A., Proceedings of the 21st IEEE Computer Security Foundations Symposium (Pittsburg, USA), 331-344, IEEE Press.
Dellis N. (2010), Using Controlled Natural Language for World Knowledge Reasoning, MSc thesis, University of Miami (Miami, USA).
Denney E., Fischer B., Schumann J. (2004), Using Automated Theorem Provers to Certify Auto-generated Aerospace Software, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 198-212, Lecture Notes in Artificial Intelligence 3097.
Dennis L., Bundy A. (2002), A Comparison of two Proof Critics: Power vs. Robustness, Carreno V., Munoz C., Tahar S., Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (Hampton, USA), 182-198, Lecture Notes in Computer Science 2410, Springer-Verlag.
Denzinger J., Kronenburg M., Schulz S. (1997), DISCOUNT: A Distributed and Learning Equational Prover, Journal of Automated Reasoning 18(2), 189-198.
Denzinger J., Schulz S. (1996), Learning Domain Knowledge to Improve Theorem Proving, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 62-76, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.
Denzinger J., Schulz S. (1996), Recording and Analysing Knowledge-based Distributed Deduction Processes, Journal of Symbolic Computation 21, 523-541.
Desharnais J., Möller B., Struth G. (2006), Kleene Algebra with Domain, ACM Transactions on Computational Logic 7(4), 798-833.
Desharnais J., Möller B., Struth G. (2004), Termination in Modal Kleene Algebra, L{\'e}vy J., Mayr E., Mitchell J., Proceedings of the 18th World Computer Congress, 3rd International Conference on Theoretical Computer Science (Toulouse, France), 647-660, Kluwer.
Desharnais J., Struth G. (2008), Modal Semirings Revisited, Audebaud P., Paulin-Mohring C., Proceedings of the 9th International Conference on the Mathematics of Program Construction (Marseille, France), 360-387, Lecture Notes in Computer Science 5133, Springer-Verlag.
Doornbos H., Backhouse R., van der Woude J. (1997), A Calculational Approach to Mathematical Induction, Theoretical Computer Science 179, 103-135.
Dowek G. (2022), From the Universality of Mathematical Truth to the Interoperability of Proof Systems, Blanchette J., Kovacs L., Pattinson D., Proceedings of the 11th International Joint Conference on Automated Reasoning (Haifa, Israel), 8-11, Lecture Notes in Artificial Intelligence 13385.
Dowek G., Hardin T., Kirchner C. (1995), Higher-order Unification via Explicit Substitutions, Kozen D., Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (San Diego, USA), 366-374, IEEE Computer Society Press.
Draeger J. (1993), Anwendung des Theorembeweisers SETHEO auf angeordnete Körper, FKI-186-93, Technische Universität München (München, Germany).
Dreben B., Goldfarb W. (1979), Decision Problem: Solvable Classes of Quantificational Formulas, 120, Addison-Wesley.
Dutertre B., de Moura L. (2006), The YICES SMT Solver, http://yices.csl.sri.com/tool-paper.pdf.
Ebner G., Hetzl S., Reis G., Riener M., Wolfsteiner S., Zivota S. (2016), System Description: GAPT 2.0, Olivetti N., Tiwari A., Proceedings of the 8th International Joint Conference on Automated Reasoning (Coimbra, Portugal), 293-301, Lecture Notes in Artificial Intelligence 9706.
Eiter T., Iannis G., Lukasiewicz T., Schindlauer R., Tompits H. (2008), Combining Answer Set Programming with Description Logics for the Semantic Web, Artificial Intelligence 172(12-13), 1495-1539.
Ernst Z. (2002), Completions from TV-> to H->, Bulletin of the Section of Logic.
Ernst Z., Fitelson B., Harris K., McCune W., Padmanabhan R., Veroff R., Wos L. (2002), More First-order Test Problems in Math and Logic, Sutcliffe G., Pelletier J., Suttner C., Proceedings of the CADE-18 Workshop - Problem and Problem Sets for ATP (Copenhagen, Denmark), Department of Computer Science, University of Copenhagen, Technical Report 02/10.
Ernst Z., Fitelson B., Harris K., Wos L. (2001), A Concise Axiomatization of RM->, Bulletin of the Section of Logic 30(4), 191-194.
Eschenbach C., Habel C., Kulik L. (1999), Representing Simple Trajectories as Oriented Curves, Russell I., Kumar A., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), 431-436, AAAI Press.
Fari{\~n}as del Cerro L., Herzig A., Longin D., Rifi O. (1998), Belief Reconstruction in Cooperative Dialogues, Giunchiglia F., Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, SYstems, and Applications (Sozopol, Bulgaria), 254-266, Lecture Notes in Computer Science 1480, Springer-Verlag.
Fellbaum C. (1998), WordNet: An Electronic Lexical Database, MIT Press.
Fermüller C., Leitsch A., Tammet T., Zamov N. (1993), Resolution Methods for the Decision Problem, Lecture Notes in Computer Science 679, Springer-Verlag.
Feys R. (1950), Les systemes formalises de modalites aristoteliciennes.
Fish A., Lisitsa A. (2014), Detecting Unknots via Equational Reasoning, I: Exploration, Watt S., Davenport J., Sexton A., Sojka P., Urban J., Proceedings of the 7th International Conference on Intelligent Computer Mathematics (Coimbra, Portugal), 76-91, Lecture Notes in Artificial Intelligence 8543, Springer-Verlag.
Fitelson B., Harris K. (2001), Distributivity in LN0 and other Sentential Logics, Journal of Automated Reasoning 27(2), 141-156.
Fitelson B., Wos L. (2001), Missing Proofs Found, Journal of Automated Reasoning 27(2), 201-225.
Fitelson B., Zalta E. (2007), Steps Toward a Computational Metaphysics, Journal of Philosophical Logic 36(2), 227-247.
Fitting M. (2007), Modal Proof Theory, Blackburn P., van Benthem J., Wolther F., Handbook of Modal Logic, 86-135, Elsevier.
Fitting M. (2002), Types, Tableaus, and Gödel’s God, Trends in Logic 12, Springer.
Fitting M. (2000), Higher-Order Modal Logic - A Sketch, Caferra R., Salzer G., Automated Deduction in Classical and Non-Classical Logics, 23-38, Lecture Notes in Artificial Intelligence 1761, Springer-Verlag.
Fitting M., Mendelsohn R. (1998), First-Order Modal Logic, Kluwer.
Fleisig S., Loveland D.W., Smiley A.K., Yarmush D.L. (1974), An Implementation of the Model Elimination Proof Procedure, Journal of the ACM 21(1), 124-139.
Font J.M., Rodriguez A.J., Torrens A. (1984), Wajsberg Algebras, Stochastica 8(1), 5-31.
Fontaine P., Merz S., Woltzenlogel Paleo B. (2011), Compression of Propositional Resolution Proofs via Partial Regularization, Bj{\o}rner N., Sofronie-Stokkermans V., Proceedings of the 23rd International Conference on Automated Deduction (Wroclaw, Poland), 237-251, Lecture Notes in Artificial Intelligence 6803, Springer-Verlag.
Forbes G. (1994), Modern Logic. A Text in Elementary Symbolic Logic, Oxford University Press.
Friedman J. (1963), A Semi-Decision Procedure for the Functional Calculus, Journal of the ACM 10(1), 1-24.
Friedrich S. (2004), Lazy Lists II, Archive of Formal Proofs, http://isa-afp.org/entries/Lazy-Lists-II.shtml.
Fuchs M. (1994), The Application of Goal-Orientated Heuristics for Proving Equational Theorems via the Unfailing Knuth-Bendix Completion Procedure. A case study: lattice ordered groups, SEKI-Report SR-94-02, Universität Kaiserslautern (Kaiserslautern, Germany).
Fuchs N., Kaljurand K., Kuhn T. (2008), Attempto Controlled English for Knowledge Representation, Baroglio C., Bonatti P., Maluszynski J., Marchiori M., Polleres A., Schaffert S., Proceedings of Reasoning Web: 4th International Summer School (Venice, Italy), 104-124, Lecture Notes in Computer Science 5224, Springer-Verlag.
Fujita M., Hasegawa R., Koshimura M., Fujita H. (1992), Model Generation Theorem Provers on a Parallel Inference Machine, Proceedings of the International Conference on Fifth Generation Computer Systems, 357-375.
Fujita M., Slaney J.K., Bennett F. (1993), Automatic Generation of Some Results in Finite Algebra, Bajcsy R., Proceedings of the 13th International Joint Conference on Artificial Intelligence (Chambery, France), 52-57, Morgan Kaufmann.
Furbach U., Glöckner I., Helbig H., Pelzer B. (2008), LogAnswer - A Deduction-based Question Answering System, Baumgartner P., Armando A., Dowek G., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), 139-146, Lecture Notes in Artificial Intelligence 5195, Springer-Verlag.
Galatos N., Jipsen P., Kowalski T., Ono H. (2007), Residuated Lattices: An Algebraic Glimpse on Substructural Logics, Studies in Logic 151, Elsevier.
Galatos N., Tsinakis C. (2005), Generalized MV-algebras, Journal of Algebra 283, 254-291.
Ganczarski J. (1996), On the Lattice of Subgroups of a Group, Journal of Formalized Mathematics 5(3), 309-312.
Garg D. (2008), Principal-Centric Reasoning in Constructive Authorization Logic, Proceedings of the LICS 2008 Workshop on Intuitionistic Modal Logics and Applications (Pittsburg, USA).
Garg D., Abadi M. (2008), A Modal Deconstruction of Access Control Logics, Amadio R., Proceedings of the 11th International Conference on the Foundations of Software Science and Computational Structures (Budapest, Hungary), 216-230, Lecture Notes in Computer Science 4962.
Gauthier T., Kaliszyk C. (2015), Premise Selection and External Provers for HOL4, Leroy X., Tiu A., Proceedings of the 4th ACM SIGPLAN Conference on Certified Programs and Proofs (Mumbai, India), 49-57, ACM Press.
Genesereth M.R., Fikes R.E. (1992), Knowledge Interchange Format, Version 3.0 Reference Manual, Logic-92-1, Computer Science Department, Stanford University.
Geuvers H. (2009), Proof Assistants: History, Ideas and Future, Sadhana 34, 3-25.
Girle R.A. (2000), Modal Logics and Philosophy, Acumen Publishers.
Glickfield B., Overbeek R. (1986), A Foray into Combinatory Logic, Journal of Automated Reasoning 2(4), 419-431.
Glöckner I. (2007), University of Hagen at CLEF 2007: Answer Validation Exercise, Nardi .A., Peters C., Working Notes for the CLEF 2007 Workshop (Budapest, Hungary).
Goldblatt R. (2006), Mathematical Modal Logic: A View of its Evolution, Gabbay D., Woods J., Logic and the Modalities in the Twentieth Century, 1-98, Handbook of the History of Logic 7, Elsevier.
Goldblatt R. (1992), Logics of Time and Computation, Center for the Study of Language and Information - Lecture Notes, The University of Chicago Press.
Goller C. (1993), Anwendung des Theorembeweisers SETHEO auf die Theorie der Halbgruppen und Gruppen, FKI-174-93, Technische Universität München (München, Germany).
Gow J., Walsh T., Colton S., Sorge V. (2003), Proceedings of the Workshop on Challenges and Novel Applications for Automated Reasoning, 19th International Conference on Automated Reasoning.
Grabowski A., Milewski R. (1997), Boolean Posets, Posets under Inclusion and Products of Relational Structures, Journal of Formalized Mathematics 6(1), 117-121.
Grewe S., Erdweg S., Wittman P., Mezini M. (2015), Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers, Murphy G., Proceedings of Onward! (Pittsburg, USA), ACM Press.
Guard J.R., Oglesby F.C., Bennett J.H., Settle L.G. (1969), Semi-Automated Mathematics, Journal of the ACM 16(1), 49-62.
Gustafsson J. (2024), A Gödelian Ontological Proof with More Plausible Axiological Principles, Ergo, To appear.
Gustafsson J. (2020), A Patch to the Possibility Part of Gödel's Ontological Proof, Analysis 80(2), 229-240.
Gustafsson J. (2020), A Paradox for the Intrinsic Value of Freedom of Choice, No{\^u}s 54(4), 891-913.
Gödel K. (1969), An Interpretation of the Intuitionistic Sentential Logic, Hintikka J., The Philosophy of Mathematics, 128-129, Oxford University Press.
Gödel K. (1933), An Interpretation of the Intuitionistic Propositional Calculus, Feferman S., Dawson J., Kleene S., Moore G., Solovay R., van Heijenoort J., Collected Works: Publications 1929-1936, Oxford University Press.
Hackstaff L. (1966), Systems of Formal Logic, Reidel Publishing.
Halleck J. (), John Halleck's Logic Systems, http://www.cc.utah.edu/~nahaj/logic/structures/systems/.
Hannan M.T. (1998), Rethinking Age Dependence in Organizational Mortality: Logical Formalizations, American Journal of Sociology 104, 126-164.
Harary F. (1969), Graph Theory, Addison-Wesley.
Harary F., Hell P. (1974), Generalized Ramsey Theory for Graphs V: The Ramsey Number of a Digraph, Bulletin of the London Mathematical Society 6, 175-182.
Hardy G.H., Wright E.M. (1992), An Introduction to the Theory of Numbers, Oxford UP.
Hayes J.P. (1993), Introduction to Digital Logic Circuit Design, Addison Wesley.
He L. (2001), I-SATCHMO: An Improvement of SATCHMO, Journal of Automated Reasoning 27(3), 313-322.
He L., Chao Y., Shimajiri Y., Seki H., Itoh H. (1998), A-SATCHMORE: SATCHMORE with Availability Checking, New Generation Computing 16, 55-74.
Heath T. (1956), The Thirteen Books of Euclid's Elements, Dover Publications.
Heinsohn J., Kudenko D., Nebel B., Profitlich H-J. (1994), An Empirical Analysis of Terminological Representation Systems, Artificial Intelligence 68(2), 367-397.
Henkin L. (1950), Completeness in the Theory of Types, Journal of Symbolic Logic 15(2), 81-91.
Henkin L., Monk J., Tarski A. (1971), Cylindrical Algebras, North-Holland.
Higman G., Neumann B.H. (1952), Groups as Groupoids with One Law, Publicationes Mathematicae Debrecen 2, 215-227.
Hilbert D., Bernays P. (1934), Grundlagen der Mathematick, Julius Springer Verlag.
Hillenbrand T., Buch A., Fettig R. (1996), On Gaining Efficiency in Completion-based Theorem Proving, Ganzinger H., Proceedings of the 7th International Conference on Rewriting Techniques and Applications (New Brunswick, USA), 432-435, Lecture Notes in Computer Science 1103, Springer-Verlag.
Hillenbrand T., Buch A., Vogt R., Löchner B. (1997), Waldmeister: High Performance Equational Deduction, Journal of Automated Reasoning 18(2), 265-270.
Hillenbrand T., Jaeger A., Löchner B. (1999), Waldmeister - Improvements in Performance and Ease of Use, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 232-236, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.
Hilpinen R. (1971), Deontic Logic: Introductory and Systematic Readings, D. Reidel.
Hoepman J-H. (1994), Uniform Deterministic Self-Stabilizing Ring-Orientation on Odd-Length Rings, Tel G., Vitanyi P., Proceedings of the 8th International Workshop on Distributed Algorithms (Terschelling, The Netherlands), 265-279, Lecture Notes in Computer Science 857, Springer-Verlag.
Hoeschele M. (2009), Towards a Semi-Automatic Higher-Order Tableau Prover, Bachelor's Thesis, Saarland University (Saarbruecken, Germany).
Homann K., Calmet J. (1996), Structures for Symbolic Mathematical Reasoning and Computation, Calmet J., Limongelli C., Proceedings of the International Symposium on the Design and Implementation of Symbolic Computation Systems (Karlsruhe, Germany), 216-227, Lecture Notes in Computer Science 1128, Springer-Verlag.
Hommersom A., Lucas P., van Bommel P. (2005), Automated Theorem Proving for Quality-checking Medical Guidelines, Sutcliffe G., Fischer B., Schulz S., Proceedings of the Workshop on Empirically Successful Classical Automated Reasoning (Tallinn, Estonia).
Horner J. (2019), A Computationally Assisted Reconstruction of an Ontological Argument in Spinoza's The Ethics, Open Philosophy 2, 219-229.
Howson A.G. (1972), A Handbook of Terms used in Algebra and Analysis, Cambrige University Press.
Huang G. (1996), Using OTTER and Prolog to Solve TopSpin, AAR Newsletter 33, 3-4.
Huang G., Myers D. (1998), Subgoal Strategies for Solving Board Puzzles, Journal of Automated Reasoning 20(3), 215-253.
Hughes G., Cresswell M. (1996), A New Introduction to Modal Logic, Methuen and Co.
Huima A., Aura T. (1997), Using Multimodal Logic to Express Conflicting Interests in Security Protocols, Orman H., Meadows C., Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (New Jersey, USA), DIMACS.
Hustadt U., Schmidt R. (2000), Issues of Decidability for Description Logics in the Framework of Resolution, Caferra R., Salzer G., Automated Deduction in Classical and Non-Classical Logics, 191-205, Lecture Notes in Artificial Intelligence 1761, Springer-Verlag.
Hustadt U., Schmidt R. (2000), MSPASS: Modal Reasoning by Translation and First-Order Resolution, Dyckhoff R., Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (St Andrews, United Kingdom), 67-71, Lecture Notes in Artificial Intelligence 1847, Springer-Verlag.
Hustadt U., Schmidt R.A. (1997), On Evaluating Decision Procedures for Modal Logics, Pollack M.E., Proceedings of the 15th International Joint Conference on Artificial Intelligence (Nagoya, Japan), 202-207, Morgan Kaufmann.
Hähnle R., Beckert B., Gerberding S. (1994), The Many-Valued Tableau-based Theorem Prover 3TAP, TR 30/94, Fakultät für Informatik, Universät Karlsruhe (Karlsruhe, Germany).
Hähnle R., Kerber M., Weidenbach C. (1996), Common Syntax of the DFG-Schwerpunktprogramm Deduction, TR 10/96, Fakultät für Informatik, Universät Karlsruhe (Karlsruhe, Germany).
Höfner P., Struth G. (2008), On Automating the Calculus of Relations, Baumgartner P., Armando A., Dowek G., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), 50-66, Lecture Notes in Artificial Intelligence 5195.
Höfner P., Struth G. (2007), Automated Reasoning in Kleene Algebra, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 279-294, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.
Höfner P., Struth G., Sutcliffe G. (2009), Automated Verification of Refinement Laws, Annals of Mathematics and Artificial Intelligence 55(1), 35-62.
ICOT (1992), Model Generation Theorem Prover, MGTP, FGCS'92 - International Conference on Fifth Generation Computer Systems, Demonstrations, 63-74.
Iwanuma K. (1997), Lemma Matching for a PTTP-based Top-down Theorem Prover, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 146-160, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.
Jakubuv J., Chvalovsk{\'y} K., Ols{\'a}k M., Piotrowski B., Suda M., Urban J. (2020), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Peltier N., Sofronie-Stokkermans V., Proceedings of the 10th International Joint Conference on Automated Reasoning (Online), 448-463, Lecture Notes in Artificial Intelligence 12167.
Jech T. (1995), Otter Experiments in a System of Combinatory Logic, Journal of Automated Reasoning 14(3), 413-426.
Jech T. (1993), LD-Algebras, Association for Automated Reasoning Newsletter 22, 9-12.
Joiner T., Walker R., Rudd M., Jobes D. (1999), Scientizing and Routinizing the Assessment of Suicidality in Outpatient Practice, Professional Psychology: Research and Practice 30(5), 447-453.
Jones L. (2004), The Encyclopedia of Religion, Macmillan.
Jones R. (1993), Little Problem, Solved by Otter, HOL mailing list http://lal.cs.byu.edu/lal/holdoc/info-hol/15xx/1572.html.
J{\'o}nsson B., Tarski A. (1951), Boolean Algebras with Operators, Part I, American Journal of Mathematics 73, 891-939.
Kalish D., Montague R. (1964), Logic: Techniques of Formal Reasoning, World, Harcourt and Brace.
Karno Z. (1996), Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space, Journal of Formalized Mathematics 5(1), 125-130.
Karno Z. (1993), Maximal Discrete Subspaces of Almost Discrete Topological Spaces, Journal of Formalized Mathematics 4(1), 125-135.
Karno Z. (1992), Continuity of Mappings over the Union of Subspaces, Journal of Formalized Mathematics 3(1), 1-16.
Kautz H., Selman B. (1996), Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search, Clancey W., Weld D., Proceedings of the 13th National Conference on Artificial Intelligence (Portland, USA), 1194-1201.
Kautz H., Selman B. (1992), Planning as Satisfiability, Neumann B., Proceedings of the 10th European Conference on Artificial Intelligence (Vienna, Austria).
Kelley J.L. (1955), General Topology, D. Van Nostrand.
Kepka T., Kunen K., Phillips J.D. (2007), The Structure of F-Quasigroups, Journal of Algebra 317, 435-461.
Kinyon M., Kunen K. (2006), Power-associative, Conjugacy Closed Loops, Journal of Algebra 304(12), 679-711.
Kinyon M., Kunen K. (2004), The Structure of Extra Loops, Quasigroups Related Systems 12, 39-60.
Kinyon M., Kunen K., Phillips J.D. (2004), Diassociativity in Conjugacy Closed Loops, Communications in Algebra 32, 767-786.
Kinyon M., Kunen K., Phillips J.D. (2002), Every Diassociative A-loop is Moufang, Proceedings of the American Mathematical Society 17(130), 619-624.
Kinyon M., Kunen K., Phillips J.D. (2002), A Generalization of Moufang and Steiner Loops, Algebra Universalis 48, 81-101.
Kinyon M., Phillips J.D. (2005), Rectangular Quasigroups and Rectangular Loops, Computers and Mathematics with Applications 49(11-12), 1679-1685.
Kinyon M., Phillips J.D. (2004), Commutants of Bol Loops of Odd Order, Proceedings of the American Mathematical Society 132, 617-619.
Kinyon M., Phillips J.D. (2004), Axioms for Trimedial Quasigroups, Commentationes Mathematicae Universitatis Carolinae 45, 287-294.
Kinyon M., Phillips J.D. (2002), A Note on Trimedial Quasigroups, Quasigroups and Related Systems 9, 65-66.
Kinyon M., Phillips J.D., Vojtechovsky P. (2008), When is the Commutant of a Bol Loop a Subloop?, Transactions of the American Mathematical Society 360(5), 2393-2408.
Kinyon M., Phillips J.D., Vojtechovsky P. (2007), C-loops: Extensions and Constructions, Journal of Algebra and its Applications 6(1), 1-20.
Kisielewicz A. (1997), Austin Identities, Algebra Universalis 38(3), 324-328.
Kobsa A., Pohl W. (1995), The User Modeling Shell System BGP-MS, Springer.
Kohlhase M. (), OMDoc: A Standard for Open Mathematical Documents, https://trac.omdoc.org/OMDoc.
Kolodner I. (1967), A Simple Proof of the Schroder-Bernstein Theorem, The American Mathematical Monthly 74(8), 995-996.
Kornilowicz A. (1996), On the Group of Inner Automorphisms, Journal of Formalized Mathematics 5(1), 43-45.
Korni{\l}owicz A. (1997), On the Topological Properties of Meet-Continuous Lattices, Journal of Formalized Mathematics 6(2), 269-277.
Korovin K., Kovac L., Reger G., Schoisswohl J., Voronkov A. (2023), ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version), EasyChair Preprints 9606, https://easychair.org/publications/preprint/KJX2.
Koshimura M., Umeda M., Hasegawa R. (2005), Abstract Model Generation of Preprocessing Clause Sets, Baader F., Voronkov A., Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Montevideo, Uruguay), 67-78, Lecture Notes in Artificial Intelligence 3452, Springer-Verlag.
Kossey I. (1997), A Note on the Completeness of Higher Order Resolution, Publicationes Mathematicae Debrecen 51(1-2).
Kotelnikov E., Kovacs L., Reger G., Voronkov A. (2016), The Vampire and the FOOL, Avigad J., Chlipala A., Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (St Petersburg, USA), 37-48, ACM.
Kotler P., Armstrong G., Brown L., Adam S. (2006), Marketing, Pearson Education.
Kovacs L., Voronkov A. (2009), Interpolation and Symbol Elimination, Schmidt R., Proceedings of the 22nd International Conference on Automated Deduction (Montreal Canada), 199-213, Lecture Notes in Artificial Intelligence 5663, Springer-Verlag.
Kozen D. (2000), On Hoare Logic and Kleene Algebra with Tests, ACM Transactions on Computational Logic 1(1), 60-76.
Kozen D. (1997), Kleene Algebra with Tests, ACM Transactions on Programming Language Systems 19(3), 427-443.
Kozen D. (1994), A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events, Information and Computation 110(2), 366-390.
Kuhn T. (2008), AceWiki: Collaborative Ontology Management in Controlled Natural Language, Lange C., Schaffert S., Skaf-Molli H., Völkel M., Proceedings of the 3rd Semangtic Wiki Workshop (Tenerife, Spain), 94-99, CEUR Workshop Proceedings 360.
Kulik L., Eschenbach C. (1999), A Geometry of Oriented Curves, Report from the project: Axiomatics of Spatial Concepts, Department for Informatics, University of Hamburg (Hamburg, USA).
Kuncak V., Hguyen H., Rinard M. (2007), Deciding Boolean Algebra with Presburger Arithmetic, Journal of Automated Reasoning 36(3), 213-239.
Kuncak V., Rinard M. (2007), Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 215-230, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.
Kunen K. (2000), The Structure of Conjugacy Closed Loops, Transactions of the American Mathematical Society 352(6), 2889-2911.
Kunen K. (1998), Alternative Loop Rings, Communications of Algebra 26(2), 557-564.
Kunen K. (1996), Moufang Quasigroups, Journal of Algebra 183(1), 231-234.
Kunen K. (1996), Quasigroups, Loops, and Associative Laws, Journal of Algebra 185(1), 194-204.
Kunen K. (1992), Single Axioms for Groups, Journal of Automated Reasoning 9(3), 291-308.
Kurosh A.G. (1956), The Theory of Groups, 99-100, Chelsea.
Külwein D., Blanchette J. (2014), A Survey of Axiom Selection as a Machine Learning Problem, Geschke S., Computability and Metamathematics : Festschrift Celebrating the 60th birthdays of Peter Koepke and Philip Welch, 1-15, College Publications.
Külwein D., Cramer M., Koepke P., Schröder B. (2010), Premise Selection in the Naproche System, Giesl J., Haehnle R., Proceedings of the 5th International Joint Conference on Automated Reasoning (Edinburgh, United Kingdom), 434-440, Lecture Notes in Artificial Intelligence 6173.
Lammich P. (2009), Collections Framework, Archive of Formal Proofs, http://isa-afp.org/entries/Collections.shtml.
Lampert T., Nakano A. (2020), Deciding Simple Infinity Axiom Sets with One Binary Relation by Superpostulates, Peltier N., Sofronie-Stokkermans V., Proceedings of the 10th International Joint Conference on Automated Reasoning (Online), 201-217, Lecture Notes in Artificial Intelligence 12166.
Landau E. (1930), Grundlagen der Analysis, Akademische Verlagsgesellschaft M.B.H.
Lawrence J.D., Starkey J.D. (1974), Experimental Tests of Resolution Based Theorem-proving Strategies., Computer Science Department, Washington State University (Pullman, USA).
Leblanc H. (1983), Alternatives to Standard First-Order Semantics, Gabbay D., Guenther F., Handbook of Philosophical Logic, 189-274, D. Reidel.
Lee S-J. (1990), CLIN: An Automated Reasoning System Using Clause Linking, PhD thesis, University of North-Carolina at Chapel Hill (Chapel Hill, USA).
Lee S-J., Plaisted D.A. (1992), Eliminating Duplication with the Hyper-Linking Strategy, Journal of Automated Reasoning 9(1), 25-42.
Leiss H. (2006), Kleene Modules and Linear Languages, Journal of Logic and Algebraic Programming 66(2), 185-194.
Letz R. (1997), LINUS: A Link Instantiation Prover with Unit Support, Journal of Automated Reasoning 18(2), 205-210.
Letz R., Mayr K., Goller C. (1994), Controlled Integration of the Cut Rule into Connection Tableau Calculi, Journal of Automated Reasoning 13(3), 297-337.
Letz R., Schumann J., Bayerl S., Bibel W. (1992), SETHEO: A High-Performance Theorem Prover, Journal of Automated Reasoning 8(2), 183-212.
Li D. (1998), A Shorter and Intuitive Axiom to Replace the Third Axiom of Compatibility of Equality with Apartness and Convergence, AAR Newsletter 39.
Li D. (1997), Replacing the Axioms for Connecting Lines and Intersection Points by Two Single Axioms, AAR Newsletter 37.
Li D. (1994), The Formulation of the Halting Problem Is Not Suitable for Describing the Halting Problem, AAR Newsletter 27, 1-7.
Li D.L., Tiu A. (2019), Combining ProVerif and Automated Theorem Provers for Security Protocol Verification, Fontaine P., Proceedings of the 27th International Conference on Automated Deduction (Natal, Brazil), 354-365, Lecture Notes in Computer Science 11716, Springer-Verlag.
Libal T. (2020), Towards Automated GDPR Compliance Checking, Heintz F., Milano M., O'Sullivan B., Proceedings of the International Workshop on the Foundations of Trustworthy AI Integrating Learning, Optimization and Reasoning (Santiago de Compostela, Spain), 3-19, Lecture Notes in Computer Science 12641.
Libal T., Steen A. (2020), Towards an Executable Methodology for the Formalization of Legal Texts, Dastani M., Dong H., van der Torre L., Proceedings of the 3rd International Conference on Logic and Argumentation (Hangzhou, China), 151-165, Lecture Notes in Computer Science 12061.
Lifschitz V. (1989), What is the Inverse Method?, Journal of Automated Reasoning 5(1), 1-24.
Litak T., Mikul{\'a}s S., Hidders J. (2016), Relational Lattices: From Databases to Universal Algebra, Journal of Logical and Algebraic Methods in Programming 85(4), 540-573.
Liu C.L. (1985), Elements of Discrete Mathematics, McGraw-Hill.
Lochbihler A. (2010), Coinductive, Archive of Formal Proofs, http://isa-afp.org/entries/Coinductive.shtml.
Longmore J.M., Hope R.A., Longmore M., Wilkinson I., Torok E. (2001), Oxford Handbook of Clinical Medicine, Oxford University Press.
Loux M. (2006), Metaphysics: A Contemporary Introduction, Routledge.
Loveland D.W. (1969), Theorem-provers Combining Model Elimination and Resolution, Machine Intelligence 4, 73-86.
Loveland D.W. (1968), Mechanical Theorem Proving by Model Elimination, Journal of the ACM 15(2), 236-251.
Luckham D. (1968), Some Tree-paring Strategies for Theorem Proving, Machine Intelligence 3, 95-112.
Lusk E.L., McCune W.W. (1993), Uniform Strategies: The CADE-11 Theorem Proving Contest, Journal of Automated Reasoning 11(3), 317-331.
Lusk E.L., McCune W.W. (1992), Experiments with ROO, a Parallel Automated Deduction System, Fronhofer B., Wrightson G., Parallelization in Inference Systems, 139-162.
Lusk E.L., Overbeek R. (1985), Non-Horn Problems, Journal of Automated Reasoning 1(1), 103-114.
Lusk E.L., Overbeek R. (1985), Reasoning about Equality, Journal of Automated Reasoning 1(2), 209-228.
Lusk E.L., Wos L. (1992), Benchmark Problems in Which Equality Plays the Major Role, Kapur D., Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), 781-785, Lecture Notes in Artificial Intelligence 607, Springer-Verlag.
Lusk E.L., Wos L. (1991), Benchmark Problems in Which Equality Plays the Major Role, MCS-P275-1191, Mathematics and Computer Science Division, Argonne National Laboratory (Argonne, USA).
Lyaletski A., Paskevich A., Verchinine K. (2006), SAD as a Mathematical Assistant - How should we go from Here to There?, Benzmüller C., Journal of Applied Logic 4(4), Towards Computer Aided Mathematics, 560-591.
MacLane S. (1971), Categories for the Working Mathematician, Springer Verlag.
Maddux R. (2006), Relation Algebras, Studies in Logic and the Foundations of Mathematics 150, Elsevier.
Maddux R. (1995), Relation-Algebraic Semantics, Theoretical Computer Science 160(1-2), 1-85.
Manes E., Benson D. (1985), The Inverse Semigroup of a Sum-ordered Semiring, Semigroup Forum 31, 129-152.
Manna Z., Pnueli A. (1990), Tools and Rules for the Practicing Verifier, CS-TR-90-1321, Department of Computer Science, Stanford University (Stanford, USA).
Manthey R., Bry F. (1988), SATCHMO: A Theorem Prover Implemented in Prolog, Lusk E., Overbeek R., Proceedings of the 9th International Conference on Automated Deduction (Argonne, USA), 415-434, Lecture Notes in Computer Science 310, Springer-Verlag.
Marasik A. (1997), Algebraic Operation on Subsets of Many Sorted Sets, Journal of Formalized Mathematics 6(3), 397-401.
Marcinkowski J., Otop J., Stelmaszek G. (2005), On a Semantic Subsumption Test, Baader F., Voronkov A., Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Montevideo, Uruguay), 142-153, Lecture Notes in Artificial Intelligence 3452, Springer-Verlag.
Matsuzaki T., Iwane H., Kobayashi M., Zhan Y., Fukasaku R., Kudo J., Anai H., Arai N. (2016), Race against the Teens - Benchmarking Mechanized Math on Pre-university Problems, Olivetti N., Tiwari A., Proceedings of the 8th International Joint Conference on Automated Reasoning (Coimbra, Portugal), 213-227, Lecture Notes in Artificial Intelligence 9706.
Matuszewski R. (1990), Formalized Mathematics, http://www.mizar.org/fm/.
McCarthy J. (1959), Programs with Common Sense, Proceedings of the Teddington Conference on the Mechanization of Thought (Teddington, United Kingdom), 75-91, Her Majesty's Stationery Office.
McCharen J., Overbeek R., Wos L. (1976), Problems and Experiments for and with Automated Theorem-Proving Programs, IEEE Transactions on Computers C-25(8), 773-782.
McCune W. (2005), Fascinating XCB Inference, Association for Automated Reasoning Newsletter.
McCune W.W. (), EQP: Equational Prover, http://www.cs.unm.edu/~mccune/eqp/.
McCune W.W. (), Otter: An Automated Deduction System, http://www.cs.unm.edu/~mccune/otter/.
McCune W.W. (2003), Mace4 Reference Manual and Guide, ANL/MCS-TM-264, Argonne National Laboratory (Argonne, USA).
McCune W.W. (1998), Automatic Proofs and Counterexamples for some Ortholattice Identities, Information Processing Letters 65.
McCune W.W. (1995), Four Challenge Problems in Equational Logic, AAR Newsletter 28, 9-10.
McCune W.W. (1994), Otter 3.0 Reference Manual and Guide, ANL-94/6, Argonne National Laboratory (Argonne, USA).
McCune W.W. (1993), Single Axioms for Groups and Abelian Groups with Various Operations, Journal of Automated Reasoning 10(1), 1-13.
McCune W.W. (1992), Automated Discovery of New Axiomatisations of the Left Group and Right Group Calculi, Journal of Automated Reasoning 9(1), 1-24.
McCune W.W. (1988), Challenge Equality Problems in Lattice Theory, Proceedings of the 9th International Conference on Automated Deduction (Argonne, USA), 704-709, Springer.
McCune W.W., Lusk E. (1992), A Challenging Theorem of Levi, AAR Newsletter 21, 8.
McCune W.W., Padmanabhan R. (1996), Automated Deduction in Equational Logic and Cubic Curves, Lecture Notes in Artificial Intelligence 1095, Springer-Verlag.
McCune W.W., Rose M., Veroff R. (), Sheffer Stroke Bases for Ortholattices, http://www.cs.unm.edu/~mccune/papers/olsax/.
McCune W.W., Veroff R., Fitelson B., Harris K., Feist A., Wos L. (2002), Short Single Axioms for Boolean Algebra, Journal of Automated Reasoning 29(1), 1-16.
McCune W.W., Wos L. (1992), Experiments in Automated Deduction with Condensed Detachment, Kapur D., Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), 209-223, Lecture Notes in Artificial Intelligence 607, Springer-Verlag.
McCune W.W., Wos L. (1988), Some Fixed Point Problems in Combinatory Logic, AAR Newsletter 10, 7-8.
McCune W.W., Wos L. (1987), A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic, Journal of Automated Reasoning 3(1), 91-107.
McKinsey J., Tarski A. (1948), Some Theorems about the Sentential Calculi of Lewis and Heyting, Journal of Symbolic Logic 13(1), 1-15.
Megill N., Pavicic M. (2000), Equations and State and Lattice Properties that hold in Infinite Dimensional Hilber Space, International Journal of Theoretical Physics 39, 2337-2379.
Meredith C.A. (1953), Single Axioms for the Systems (C,N), (C,0), and (A,N) of the Two-valued Propositional Calculus, Journal of Computing Systems 1, 155-164.
Meredith C.A., Prior A.N. (1968), Equational Logic, Notre Dame Journal of Formal Logic 9, 212-226.
Michie D., Ross R., Shannan G.J. (1972), G-deduction, Machine Intelligence 7, 141-165.
Miller R., Shanahan M. (2002), Some Alternative Formulations of the Event Calculus, Kakas A.C., Sadri F., Computational Logic: Logic Programming and Beyond, 452-490, Lecture Notes in Artificial Intelligence 2407, McGraw-Hill.
Mitchell B. (1967), Theory of Categories, Pure and Applied Mathematics 17, Academic Press.
Montague R. (1955), On the Paradox of Grounded Classes, Journal of Symbolic Logic 20, 140.
Morgan C. (1984), Logic Problems, AAR Newsletter 3, 5-5.
Mueller E. (2004), A Tool for Satisfiability-based Commonsense Reasoning in the Event Calculus, Barr V., Markov Z., Proceedings of the 17th International FLAIRS Conference (Miami, USA), 147-152, AAAI Press.
Mueller E., Sutcliffe G. (2005), Reasoning in the Event Calculus using First-Order Automated Theorem Proving, Russell I., Markov Z., Proceedings of the 18th International FLAIRS Conference (Clearwater Beach, USA), 840-841, AAAI Press.
Mueller E., Sutcliffe G. (2005), Discrete Event Calculus Deduction using First-Order Automated Theorem Proving, Konev B., Schulz S., Proceedings of the 5th International Workshop on the Implementation of Logics (Montevideo, Uruguay), 43-56.
Mundici D. (2011), Advanced Łukasiewicz calculus and MV-algebras, Springer.
Munkres J.R. (1975), Topology: A First Course, Prentice-Hall.
Möller B. (2004), Lazy Kleene Algebra, Kozen D., Proceedings of the 7th International Conference on the Mathematics of Program Construction (Stirling, United Kindom), 252-273, Lecture Notes in Computer Science 3125, Springer-Verlag.
Möller B., Struth G. (2006), Algebras of Modal Operators and Partial Correctness, Theoretical Computer Science 351(2), 221-239.
Nalon C., Hustadt U., Papacchini F., Dixon C. (2023), Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic, Pientka B., Tinelli C., Proceedings of the 29th International Conference on Automated Deduction (Rome, Italy), 382-400, Lecture Notes in Computer Science Proceedings of the 29th International Confere, Springer-Verlag.
Nalon C., Hustadt U., Papacchini F., Dixon C. (2022), Local Reductions for the Modal Cube, Blanchette J., Kovacs L., Pattinson D., Proceedings of the 11th International Joint Conference on Automated Reasoning (Haifa, Israel), 486-505, Lecture Notes in Artificial Intelligence 13385.
National Geographic Society (1999), National Geographic Desk Reference, National Geographic Society.
Nelson S. (2008), MeSH 2008-2009, Development and Future Plans, Presentation at the Web Conference of the National Network of Libraries of Medicine, Southeastern Atlantic Region (Bethesda, USA).
Neugebauer G. (1994), XTPTP-An X Window Interface for the TPTP Library, IMN, HTWK Leipzig (Leipzig, Germany).
Neumann B.H. (1986), Yet Another Single Law for Groups, Illinois Journal of Mathematics 30(2), 295-300.
Neumann B.H. (1981), Another Single Law for Groups, Bulletin of the Australian Maths Society 23, 81-102.
Neumann J. von (1925), Eine Axiomatisierung der Mengenlehre, Journal für die reine und angewandte Mathematik 154, 219-240.
Newell A., Shaw J.C., Simon H.A. (1963), Empirical Explorations with the Logic Theory Machine: A Case Study in Heuristics, Feigenbaum E.A., Feldman J., Computers and Thought, 109-133, McGraw-Hill.
Newell A., Simon H. (1972), Human Problem Solving, Prentice-Hall.
Nieuwenhuis R., Rivero J.M., Vallejo M.A. (1997), Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.
Niles I., Pease A. (2001), Towards A Standard Upper Ontology, Welty C., Smith B., Proceedings of the 2nd International Conference on Formal Ontology in Information Systems (Ogunquit, USA), 2-9.
Nipkow T. (2021), Teaching Algorithms and Data Structures with a Proof Assistant, Hritcu A., Popescu A., Proceedings of 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, USA), 18-33, Lecture Notes in Artificial Intelligence 5195, Springer-Verlag.
Nipkow T. (2014), Amortized Complexity Verified, Archive of Formal Proofs, http://isa-afp.org/entries/Amortized_Complexity.shtml.
Nipkow T. (2009), Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite, Journal of Automated Reasoning 43(3), 289-304.
Nipkow T. (2008), Linear Quantifier Elimination, Baumgartner P., Armando A., Dowek G., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), 18-33, Lecture Notes in Artificial Intelligence 5195, Springer-Verlag.
Nonnengart A., Rock G., Weidenbach C. (1998), On Generating Small Clause Normal Forms, Kirchner C., Kirchner H., Proceedings of the 15th International Conference on Automated Deduction (Lindau, Germany), 397-411, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag.
O'Rourke P. (1989), LT Revisited: Explanation-based Learning and the Logic of Principia Mathematica, Machine Learning 4, 117-159.
Ohlbach H.J. (1985), Predicate Logic Hacker Tricks, Journal of Automated Reasoning 1(4), 435-440.
Ohlbach H.J., Schmidt R.A. (1995), Functional Translation and Second-Order Frame Properties of Modal Logics, MPI-I-95-2-002, Max-Planck-Institut für Informatik (Saarbrücken, Germany).
Ohlbach H.J., Schmidt-Schauss M. (1985), The Lion and the Unicorn, Journal of Automated Reasoning 1(3), 327-332.
Oppenheimer P., Zalta E. (2011), A Computationally-Discovered Simplification of the Ontological Argument, Australasian Journal of Philosophy 89(2), 333-349.
Ortner V., Schirmer N. (2008), BDD Normalisation, Archive of Formal Proofs, http://isa-afp.org/entries/BDD.shtml.
Otter, The problem collection distributed with the Otter ATP system [McC90].
Overbeek R. (1993), The CADE-11 Competitions: A Personal View, Journal of Automated Reasoning 11(3), 315-316.
Overbeek R. (1990), ATP competition announced at CADE-10.
Overbeek R., McCharen J., Wos L. (1976), Complexity and Related Enhancements for Automated Theorem-Proving Programs, Computers and Mathematics with Applications 2, 1-16.
Padlewska B. (1991), Locally Connected Spaces, Journal of Formalized Mathematics 2(1), 93-96.
Padlewska B. (1990), Families of Sets, Journal of Formalized Mathematics 1(1), 147-152.
Padlewska B., Darmochwa{\l} A. (1990), Topological Spaces and Continuous Functions, Journal of Formalized Mathematics 1(1), 223-230.
Padmanabhan R., McCune B., Veroff R. (2005), Levi's Commutator Theorems for Cancellative Semigroups, Semigroup Forum 71, 152-157.
Padmanabhan R., Penner P. (2000), A Hyperbase for Binary Lattice Hyperidentities, Journal of Automated Reasoning 24(3), 365-370.
Paramasivam M., Plaisted D. (1995), Automated Deduction Techniques for Classification in Concept Languages.
Paskevich A., Verchinine K., Lyaletski A., Anisimov A. (2007), Reasoning Inside a Formula and Ontological Correctness of a Formal Mathematical Text, Kauers M., Kerber M., Miner R., Windsteiger W., Calculemus/MKM 2007 - Work in Progress, 77-91, University of Linz (Linz, Austria).
Paulson L. (1996), ML for the Working Programmer, Cambridge University Press.
Pease A. (2011), Ontology: A Practical Guide, Articulate Software Press.
Pease A., Sutcliffe G. (2007), First Order Reasoning on a Large Ontology, Urban J., Sutcliffe G., Schulz S., Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Bremen, German), 61-70, CEUR Workshop Proceedings 257.
Peli G., Bruggeman J., Masuch M., O Nuallain B. (1994), A Logical Approach to Formalizing Organizational Ecology: Formalizing the Inertia-Fragment in First-Order Logic, American Sociological Review 59(2).
Peli G., Bruggeman J., Masuch M., O Nuallain B. (1992), A Logical Approach to Formalizing Organizational Ecology: Formalizing the Inertia-Fragment in First-Order Logic, CCSOM Preprint 92-74, Department of Statistics and Methodology, University of Amsterdam.
Peli G., Masuch M. (1994), The Logic of Propogation Strategies: Axiomatizing a Fragment of Organization Ecology in First-Order Logic, Moore D.P., Academy Of Management: Best Papers Proceedings 1994, 218-222.
Peli G., Masuch M. (1993), The Logic of Propogation Strategies: Axiomatizing a Fragment of Organizational Ecology in First-Order Logic, CCSOM Report 93-100, Department of Statistics and Methodology, University of Amsterdam.
Pelletier F.J. (1988), Errata, Journal of Automated Reasoning 4(2), 235-236.
Pelletier F.J. (1987), Further Developments in THINKER, and Automated Theorem Prover, TR-ARP-16/87, Automated Reasoning Project, Australian National University (Canberra, Australia).
Pelletier F.J. (1986), Seventy-five Problems for Testing Automatic Theorem Provers, Journal of Automated Reasoning 2(2), 191-216.
Pelletier F.J. (1982), Completely Non-clausal, Completely Heuristically Driven Automatic Theorem Proving, TR82-7, Department of Computer Science, Edmonton, Alberta.
Pelletier F.J., Rudnicki P. (1986), Non-Obviousness, Association for Automated Reasoning Newsletter, 4-5.
Pelletier F.J., Sutcliffe G., Hazen A.P. (2017), Automated Reasoning for the Dialetheic Logic RM3, Rus V., Markov Z., Proceedings of the 30th International FLAIRS Conference (Marco Island, USA), 110-115.
Peltier N. (1998), A New Method for Automated Finite Model Building Exploiting Failures and Symmetries, Journal of Logic and Computation 8(4), 511-543.
Pelzer B., Wernhard C. (2007), System Description: E-KRHyper, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 508-513, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.
Peterson G., Stickel M.E. (1981), Complete Sets of Reductions for Some Equational Theories, Journal of the ACM 28(8), 233-264.
Pfenning F. (1988), Single Axioms in the Implicational Propositional Calculus, Lusk E., Overbeek R., Proceedings of the 9th International Conference on Automated Deduction (Argonne, USA), 710 - 713, Lecture Notes in Computer Science 310, Springer-Verlag.
Phillips J.D. (2006), A Short Basis for the Variety of WIP PACC-loops, Quasigroups and Related Systems 14, 73-80.
Phillips J.D. (2006), Short Equational Bases for Two Varieties of Groupoids Associated with Involuted Restrictive Bisemigroups of Binary Relations, Semigroup Forum 73(2), 308-312.
Phillips J.D., Stanovsky D. (2008), Automated Theorem Proving in Loop Theory, Sutcliffe G., Colton S., Schulz S., Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics (Birmingham, United Kingdom), 42-53, CEUR Workshop Proceedings 378.
Phillips J.D., Stanovsky D. (2008), Using Automated Theorem Provers in Nonassociative Algebra, Cervesato I., Veith H., Voronkov A., Short Papers of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Doha, Qatar), Cool Press.
Phillips J.D., Vojtechovsky P. (2008), A Scoop from Groups: New Equational Foundations for Loops, Commentationes Mathematicae Universitatis Carolinae 49(2), 279-290.
Phillips J.D., Vojtechovsky P. (2006), C-loops: an Introduction, Publicationes Mathematicae Debrecen 68(1-2), 115-137.
Phillips J.D., Vojtechovsky P. (2005), The Varieties of Quasigroups of Bol-Moufang Type: An Equational Reasoning Approach, Journal of Algebra 293, 17-33.
Phillips J.D., Vojtechovsky P. (2005), The Varieties of Loops of Bol-Moufang Type, Algebra Universalis 54(3), 259-271.
Pierce B. (2002), Programming Languages, MIT Press.
Piotrowski B., Urban J. (2020), Stateful Premise Selection by Recurrent Neural Networks, Alpert E., Kovacs L., Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Online), 409-422, EPiC Series in Computing 73.
Plaisted D.A. (1994), The Search Efficiency of Theorem Proving Strategies, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 57-71, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.
Plaisted D.A. (1988), Non-Horn Clause Logic Programming Without Contrapositives, Journal of Automated Reasoning 4(3), 287-325.
Plaisted D.A. (1982), A Simplified Problem Reduction Format, Artificial Intelligence 18, 227-261.
Plaisted D.A. (1981), Theorem Proving with Abstraction, Artificial Intelligence 16, 47-108.
Pollock J.L. (1990), Interest Driven Suppositional Reasoning, Journal of Automated Reasoning 6(4), 419-461.
Popkorn S. (1995), First Steps in Modal Logic, Cambridge University Press.
Popplestone R.J. (1970), Freddy, Things and Sets.
Prasetya W. (1993), How to get FAUST?, HOL mailing list http://lal.cs.byu.edu/lal/holdoc/info-hol/15xx/1515.html.
Prevosto V., Waldmann U. (2006), SPASS+T, Sutcliffe G., Schmidt R., Schulz S., Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning (Seattle, USA), 19-33, CEUR Workshop Proceedings 192.
Puzis Y., Gao Y., Sutcliffe G. (2006), Automated Generation of Interesting Theorems, Sutcliffe G., Goebel R., Proceedings of the 19th International FLAIRS Conference (Melbourne Beach, USA), 49-54, AAAI Press.
Quaife A. (1992), Automated Development of Fundamental Mathematical Theories, Kluwer Academic Publishers.
Quaife A. (1992), Automated Deduction in von Neumann-Bernays-Godel Set Theory, Journal of Automated Reasoning 8(1), 91-147.
Quaife A. (1992), Problems based on NBG Set Theory.
Quaife A. (1990), Andrews' Challenge Problem Revisited, AAR Newsletter 15, 3-7.
Quaife A. (1989), Automated Development of Tarski's Geometry, Journal of Automated Reasoning 5(1), 97-118.
Quine W.V. (1982), Methods of Logic, 183, Harvard University Press.
Quine W.V. (1969), Set Theory and its Logic, Harvard University Press.
Rabe F. (2006), Towards Determining the Subset Relation between Propositional Modal Logics, Sutcliffe G., Schmidt R., Schulz S., Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning (Seattle, USA), CEUR Workshop Proceedings 192.
Radziszowski S. (2006), Small Ramsey Numbers, Journal of Combinatorics, Dynamic Surveys DS1.
Ramachandran D., Reagan P., Goolsbey K. (2005), First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base, Shvaiko P., Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (Pittsburgh, USA).
Randell D., Cui Z., Cohn A. (1992), A Spatial Logic Based on Regions and Connection, Nebel B., Swartout W., Proceedings of the 3rd International Conference on the Principles of Knowledge Representation and Reasoning (Cambridge, USA), 165-176, Morgan-Kaufmann.
Raths T., Otten J. (2012), The QMLTP Problem Library for First-Order Modal Logics, Gramlich B., Miller D., Sattler U., Proceedings of the 6th International Joint Conference on Automated Reasoning (Manchester, United Kingdom), 454-461, Lecture Notes in Artificial Intelligence 7364, Springer-Verlag.
Raths T., Otten J., Kreitz C. (2007), The ILTP Problem Library for Intuitionistic Logic - Release v1.1, Journal of Automated Reasoning 38(1-2), 261-271.
Reagan Smith P., Sutcliffe G., Goolsbey K., Kahlert R.C. (), The Cyc TPTP Challenge Problem Set, http://www.opencyc.org/doc/tptp_challenge_problem_set.
Reboh R., Raphael B., Yates R.A., Kling R.E., Velarde C. (1972), Study of Automatic Theorem Proving Programs, Technical Note 72, Artificial Intelligence Center, SRI International (Menlo Park, CA).
Rector A., Drummond N., Horridge M., Rogers J., Knublauch H., Stevens R., Wang H., Wroe C. (2004), OWL Pizzas: Practical Experience of Teaching OWL-DL: Common Errors & Common Patterns, Motta E., Shadbolt N., Stutt A., Gibbins N., Proceedings of the 14th International Conference on Engineering Knowledge in the Age of the Semantic Web (Whittlebury Hall, United Kingdom), 63-81, Lecture Notes in Computer Science 3257, Springer-Verlag.
Reece J., Urry L., Cain M., Wasserman S., Minorsky P., Jackson R. (2013), Campbell Biology, Benjamin-Cummings.
Reiter R. (2001), Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems, MIT Press.
Reiter R. (1992), What Should a Database Know?, Journal of Logic Programming 14(1-2), 127-153.
Retel K. (2005), Properties of First and Second Order Cutting of Binary Relations, Journal of Formalized Mathematics 13(3), 361-365.
Robinson J.A. (1963), Theorem Proving on the Computer, Jounal of the ACM 10(2), 163-174.
Rodrigues O., Russo A. (1998), A Translation Method for Belnap Logic, DoC 98/7, Imperial College London.
Romanowicz K., Grabowski A. (2004), The Operation of Addition of Relational Structures, Journal of Formalized Mathematics 12(3), 335-339.
Rose M., Wilkinson K. (2001), Application of Model Search to Lattice Theory, Association for Automated Reasoning Newsletter 52.
Ross K.A. (1990), Elementary Analysis: The Theory of Calculus, Springer.
Rubin A., Rubin J. (1993), Weak Forms of the Axiom of Choice and the Generalized Continuum Hypothesis, Mathematical Logic Quarterly 39(1), 7-22.
Rudnicki P. (1998), Representation Theorem for Free Continuous Lattices, Journal of Formalized Mathematics 7(2), 185-188.
Russell B. (1985), The Philosophy of Logical Atomism, Open Court.
Russell B., Whitehead A. (1910), Principia Mathematica, Cambridge University Press.
Russell S.J., Norvig P. (1995), Artificial Intelligence: a modern approach, Prentice-Hall.
Ryan P., Schneider S. (1998), An Attack on a Recursive Authentication Protocol: A Cautionary Tale, Information Processing Letters 65(1), 7-10.
Rybalchenko A., Navarro Perez J. (2011), Separation Logic + Superposition Calculus = Heap Theorem Prover, Cervesato I., Veith H., Voronkov A., Proceedings of the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation, To appear, ACM Press.
Sahami M. (2006), Mining the Web to Determine Similarity Between Words, Objects, and Communities, Sutcliffe G., Goebel R., Proceedings of the 19th International FLAIRS Conference (Melbourne Beach, USA), 14-19, AAAI Press.
Schey J. (1999), Introduction to Manufacturing Processes, McGraw-Hill.
Schlichtkrull A., Blanchette J., Traytel D., Waldmann U. (2018), Formalizing Bachmair and Ganzinger's Ordered Resolution Prover, Galmiche D., Schulz S., Sebastiani R., Proceedings of the 9th International Joint Conference on Automated Reasoning (Oxford, United Kingdom), 88-107, Lecture Notes in Computer Science 10900.
Schmidt G., Str{\"}ohlein T. (1993), Relations and Graphs: Discrete Mathematics for Computer Scientists, Springer-Verlag.
Schmidt R. (1999), Decidability by Resolution for Propositional Modal Logics, Journal of Automated Reasoning 22(4), 379-396.
Schulz S. (1995), Explanation Based Learning for Distributed Equational Deduction, MSc thesis, Universität Kaiserslautern.
Schulz S., Bonacina M.P. (2005), On Handling Distinct Objects in the Superposition Calculus, Konev B., Schulz S., Proceedings of the 5th International Workshop on the Implementation of Logics (Montevideo, Uruguay), 66-77.
Schwabbauser W., Szmielew W., Tarski A. (1983), Metamathematische Methoden in der Geometrie, Springer-Verlag.
Schwarzweller C. (2001), A Characterization of Concept Lattices. Dual Concept Lattices, Journal of Formalized Mathematics 9(1), 55-59.
Scott D. (1979), Identity and Existence in Intuitionist Logic, Fournam M.P., Durham Proceedings Applications of Sheaves, 660-696, Lecture Notes in Mathematics Volume 753, Springer.
Segerberg K. (1973), Two-Dimensional Modal Logic, Journal of Philosophical Logic 2(1), 77-96.
Segre A., Elkan C. (1994), A High-Performance Explanation-based Learning Algorithm, Artificial Intelligence 69(1-2), 1-50.
Seidl M., Lonsing F., Biere A. (2012), Tool for Generating EPR Formulas from QBF, Fontaine P., Schmidt R., Schulz S., Proceedings of the 3rd Workshop on Practical Aspects of Automated Reasoning (Manchester, England), 139-148.
SETHEO, AR Research Group, Technische Universität München, Problem Library, No longer available.
Shanahan M. (1997), Solving the Frame Problem, MIT Press.
Shen W. (2006), Automated Proofs of Equivalence of Modal Logic Systems, MSc thesis, Department of Computer Science, University of Miami (Miami, USA).
Shostak R.E. (1976), Refutation Graphs, Artificial Intelligence 7, 51-64.
Sider T. (2010), Logic for Philosophy, Oxford University Press.
Siekman J., Benzmüller C., Fiedler A., Meier A., Normann I., Pollet M. (2003), Proof Development with Omega: The Irrationality of Root2, Kamareddine F., Thirty Five Years of Automating Mathematics, 271-314, Kluwer Applied Logic Series 28, Kluwer Academic Publishers.
Siklossy L., Rich A., Marinov V. (1973), Breadth First Search: Some Surprising Results, Artificial Intelligence 4, 1-27.
Skorulski B. (2001), The Tichonov Theorem, Journal of Formalized Mathematics 9(2), 373-376.
Slagle J.R. (1967), Automatic Theorem Proving with Renamable and Semantic Resolution, Journal of the ACM 14(4), 687-697.
Slaney J.K. (2002), More Proofs of an Axiom of \Lukasiewicz, Journal of Automated Reasoning 29(1), 59-66.
Slaney J.K. (1993), SCOTT: A Model-Guided Theorem Prover, Bajcsy R., Proceedings of the 13th International Conference on Artificial Intelligence (Chambery, France), 109-114, Morgan-Kaufmann.
Slaney J.K. (1992), FINDER (Finite Domain Enumerator): Notes and Guide, TR-ARP-1/92, Automated Reasoning Project, Australian National University (Canberra, Australia).
Slaney J.K., Fujita M., Stickel M.E. (1995), Automated Reasoning and Exhaustive Search: Quasigroup Existence Problems, Computers and Mathematics with Applications 29(2), 115-132.
Slaney J.K., Hodgson K. (1997), Extending SCOTT to use Multiple Models, Pollack M.E., Proceedings of the 15th International Joint Conference on Artificial Intelligence (Nagoya, Japan), ???-???, Morgan Kaufmann.
Slaney J.K., Lusk E., McCune W.W. (1994), SCOTT: Semantically Constrained Otter, System Description, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 764-768, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.
Smith P. (2007), An Introduction to Goedel's Theorems, Cambridge University Press.
Smullyan R.M. (1987), Forever Undecided - A Puzzle Guide to Godel, Knopf.
Smullyan R.M. (1978), What is the Name of This Book? The Riddle of Dracula and Other Logical Puzzles, Prentice-Hall.
Smullyan R.M. (1978), To Mock a Mocking Bird and Other Logic Puzzles, Knopf.
Smullyan R.M. (1968), First-Order Logic, Springer-Verlag.
Soboci{\'n}ski B. (1952), Axiomatization of a Partial System of Three-valued Calculus of Propositions`, Journal of Computing Systems 1, 23-55.
Socher-Ambrosius R. (1992), How to Avoid the Derivation of Redundant Clauses in Reasoning Systems, Journal of Automated Reasoning 9(1), 77-97.
SPRFN, The Problem Collection Distributed with the SPRFN ATP System, https://www.cs.unc.edu/Research/mi/mi-provers.html.
Stanovsky D. (2008), Distributive Groupoids are Symmetric-by-medial: An Elementary Proof, Commentationes Mathematicae Universitatis Carolinae 49(4), 541-546.
Steel G. (2005), Deduction with XOR Constraints in Security API Modelling, Nieuwenhuis R., Proceedings of the 20th International Conference on Automated Deduction (Tallinn, Estonia), 322-336, Lecture Notes in Artificial Intelligence 3632, Springer-Verlag.
Sterling L., Shapiro E. (1986), The Art of Prolog, MIT Press.
Stevens R.L. (1992), Unpublished Note.
Stevens R.L. (1988), Challenge Problems from Nonassociative Rings for Theorem Provers, Lusk E., Overbeek R., Proceedings of the 9th International Conference on Automated Deduction (Argonne, USA), 730-734, Lecture Notes in Computer Science 310, Springer-Verlag.
Stevens R.L. (1987), Some Experiments in Nonassociative Ring Theory with an Automated Theorem Prover, Journal of Automated Reasoning 3(2), 211-221.
Stickel M.E. (1994), Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction, Journal of Automated Reasoning 13(2), 189-210.
Stickel M.E. (1986), Schubert's Steamroller Problem: Formulations and Solutions, Journal of Automated Reasoning 2(1), 89-101.
Stickel M.E. (1984), A Prolog Technology Theorem Prover, New Generation Computing 2(4), 371-383.
Stoller S. (1997), Leader Election in Distributed Systems with Crash Failures, TR481, Department of Computer Science, Indiana University (Bloomington, USA).
Stone M. (2000), Towards a Computational Account of Knowledge, Action and Inference in Instructions, Journal of Language and Computation 1, 231-246.
Stone M. (1999), Indefinite Information in Modal Logic Programming, TR-56, Rutgers University (New Brunswick, USA).
Stone M. (1998), Abductive Planning with Sensing, Mostow J., Rich C., Proceedings of the 15th Conference on Artificial Intelligence (Madison, USA), 631-636, AAAI Press.
Stone M. (1997), Applying Theories of Communicative Action in Generation Using Logic Programming, Traum D., Proceedings of the AAAI Fall Symposium On Communicative Action in Humans and Machines (Cambridge, USA), AAAI Press.
Struth G. (2008), Modal Tools for Separation and Refinement, Boiten E., Derrick J., Schellhorn G., Proceedings of the 13th BAC-FACS Refinement Workshop (Turku, Finland), 81-101, Electronic Notes in Theoretical Computer Science 214, Elsevier.
Struth G. (2007), Reasoning Automatically about Termination and Refinement, Ranise S., Proceedings of the 6th International Workshop on First-Order Theorem Proving (Liverpool, United Kingdom), 36-51.
Struth G. (2006), Abstract Abstract Reduction, Journal of Logic and Algebraic Programming 66(2), 239-270.
Suchanek F., Kasneci G., Weikum G. (2007), YAGO: A Core of Semantic Knowledge, Patel-Schneider P., Shenoy P., Proceedings of the 16th International World Wide Web Conference (Banff, Canada), 697-706.
Sussman G.J. (1973), A Computational Model of Skill Acquisition, 297, MIT Artificial Intelligence Laboratory.
Sutcliffe G. (2017), The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0, Journal of Automated Reasoning 59(4), 483-502.
Sutcliffe G. (2009), The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0, Journal of Automated Reasoning 43(4), 337-362.
Sutcliffe G. (2008), The SZS Ontologies for Automated Reasoning Software, Sutcliffe G., Rudnicki P., Schmidt R., Konev B., Schulz S., Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics (Doha, Qatar), 38-49, CEUR Workshop Proceedings 418.
Sutcliffe G., Gao Y., Colton S. (2003), A Grand Challenge of Theorem Discovery, Gow J., Walsh T., Colton S., Sorge V., Proceedings of the Workshop on Challenges and Novel Applications for Automated Reasoning (Miami, USA), 1-11.
Sutcliffe G., Melville S. (1996), The Practice of Clausification in Automatic Theorem Proving, South African Computer Journal 18, 57-68.
Sutcliffe G., Pelletier F.J., Hazen A.P. (2018), Making Belnap's "Useful Four-Valued Logic" Useful, Brawner K., Rus V., Proceedings of the 31st International FLAIRS Conference (Melbourne, USA), 116-121.
Sutcliffe G., Puzis Y. (2007), SRASS - a Semantic Relevance Axiom Selection System, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 295-310, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.
Sutcliffe G., Suda M., Teyssandier A., Dellis N., de Melo G. (2010), Progress Towards Effective Automated Reasoning with World Knowledge, Murray C., Guesgen H., Proceedings of the 23rd International FLAIRS Conference (Daytona Beach, USA), 110-115, AAAI Press.
Sutcliffe G., Suttner C.B. (1998), The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21(2), 177-203.
Sutcliffe G., Yerikalapudi A., Trac S. (2009), Multiple Answer Extraction for Question Answering with Automated Theorem Proving Systems, Guesgen H., Lane C., Proceedings of the 22nd International FLAIRS Conference (Sanibel Island, USA), 105-110, AAAI Press.
Sutcliffe G., Zimmer J., Schulz S. (2003), Communication Formalisms for Automated Theorem Proving Tools, Sorge V., Colton S., Fisher M., Gow J., Proceedings of the Workshop on Agents and Automated Reasoning (Acapulco, Mexico), 52-57.
Suttner C.B. (1995), Parallelization of Search-based Systems by Static Partitioning with Slackness, PhD thesis, Institut für Informatik, Technische Universität München (Munich, Germany), and Dissertationen zur künstlichen Intelligenz 101, Springer-Verlag.
Svensson H. (2008), A Semi-Automatic Correctness Proof Procedure applied to Stoller's Leader Election Algorithm, Technical Report 2008:7, Computer Science and Engineering, Chalmers University of Technology (Goteborg, Sweden).
Tarski A. (1959), What is Elementary Geometry?, Henkin L., Proceedings of an International Symposium. The axiomatic method with special reference to geometry and physics.
Tarski A. (1951), A Decision Method for Elementary Algebra and Geometry, University of California Press.
Tarski A. (1941), On the Calculus of Relations, Journal of Symbolic Logic 6(3), 73-89.
Tarski A. (1938), Ein Beitrag zur Axiomatik der Abelschen Gruppe n, Fundamenta Mathematicae 30, 253-256.
Tarski A. (1938), Über unerreichbare Kardinalzahlen, Fundamenta Mathematicae 30, 68-89.
Teichmann J., Evans K. (1999), Philosophy: A Beginner's Guide, Blackwell.
Terese (2003), Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press.
Troelstra A., Schwichtenberg H. (2000), Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science 43, Cambridge University Press.
Trybulec A. (1997), Moore-Smith Convergence, Journal of Formalized Mathematics 6(2), 213-225.
Trybulec A. (1992), Some Isomorphisms Between Functor Categories, Journal of Formalized Mathematics 3(1), 33-40.
Trybulec A. (1990), Enumerated Sets, Journal of Formalized Mathematics 1(1), 25-34.
Trybulec A. (1990), Tarski Grothendieck Set Theory, Journal of Formalized Mathematics 1(1), 9-11.
Trybulec A. (1990), Tuples, Projections and Cartesian Products, Journal of Formalized Mathematics 1(1), 97-105.
Trybulec A., Darmochwal A. (1990), Boolean Domains, Journal of Formalized Mathematics 1(1), 187-190.
Trybulec A., Swieczkowska H. (1989), Boolean Properties of Sets, Journal of Formalized Mathematics 1(1), 17-23.
Trybulec W., Bancerek G. (1990), Kuratowski - Zorn Lemma, Journal of Formalized Mathematics 1(2), 387-393.
Trybulec Z. (1990), Properties of Subsets, Journal of Formalized Mathematics 1(1), 67-71.
Tsarkov D., Riazanov A., Bechhofer S., Horrocks I. (2004), Using Vampire to Reason with OWL, McIlraith S., Plexousakis D., van Harmelen F., Proceedings of the 3rd International Semantic Web Conference (Hiroshima, Japan), 471-485, Lecture Notes in Computer Science 3298, Springer-Verlag.
Tseitin G.S. (1983), On the Complexity of Derivations in Propositional Calculus, Siekmann J., Wrightson G., The Automation of Reasoning, Springer-Verlag.
Urban J. (2006), MPTP 0.2: Design, Implementation, and Initial Experiments, Journal of Automated Reasoning 37(1-2), 21-43.
Urban J., Rudnicki P., Sutcliffe G. (2013), ATP and Presentation Service for Mizar Formalizations, Journal of Automated Reasoning 50(2), 229-241.
Urquhart A. (1987), Hard Problems for Resolution, Journal of the ACM 34(1), 209-219.
van Benthem J. (1979), Checking Landau's "Grundlagen" in the AUTOMATH System, Math. Centre Tracts 83, PhD thesis, Eindhoven University (Eindhoven, The Netherlands).
van Ditmarsch H., Halpern J., van der Hoek W., Kooi B. (2015), Handbook of Epistemic Logic, College Publications.
van Ditmarsch H., Kooi B. (2006), The Secret of My Success, Synthese 151(2), 201-232.
van Ditmarsch H., van de Hoek W., Kooi B. (2007), Dynamic Epistemic Logic, Springer.
Verchinine K., Lyaletski A., Paskevich A. (2007), System for Automated Deduction (SAD): A Tool for Proof Verification, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 398-403, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.
Verchinine K., Lyaletski A., Paskevich A., Anisimov A. (2008), On Correctness of Mathematical Texts from a Logical and Practical Point of View, Autexier S., Campbell J., Rubio J., Sorge V., Suzuki M., Wiedijk F., Proceedings of the Conference on Intelligent Computer Mathematics (Birmingham, United Kingdon), 583-598, Lecture Notes in Computer Science 5144, Springer-Verlag.
Veroff R. (2001), A Strategy for Proving Theorems in Many-Valued Logic, AAR Newsletter 53.
Veroff R. (1994), Problem Set, AAR Newsletter 24, 8.
Veroff R., McCune W. (), First-order Proof of a Median Algebra Problem, http://www.cs.unm.edu/~veroff/MEDIAN_ALGEBRA/.
von Luxburg U. (2007), A Tutorial on Spectral Clustering, Statistics and Computing 17(4), 395-416.
von Oheimb D., Nipkow T. (1999), Machine-Checking the Java Specification: Proving Type-Safety, Alves-Foss J., Formal Syntax and Semantics of Java, 119-156, Lecture Notes in Computer Science.
von Plato J. (1998), A Constructive Theory of Ordered Affine Geometry, Indagationes Mathematicae 9, 549-562.
von Plato J. (1995), The Axioms of Constructive Geometry, Annals of Pure and Applied Logic 76(2), 169-200.
von Wright J. (2002), From Kleene Algebra to Refinement Algebra, Boiten E., Möller B., Proceedings of the 6th International Conference on the Mathematics of Program Construction (Dagstuhl, Germany), 233-262, Lecture Notes in Computer Science 2386.
Vukmirovi{\'c} P., Bentkamp A., Nummelin V. (2020), Efficient Full Higher-order Unification, Ariola Z.M., Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (Online), 5:1-5:20, Leibniz International Proceedings in Informatics 167, Dagstuhl Publishing.
Walijewski J. (1993), Representation Theorem for Boolean Algebras, Journal of Formalized Mathematics 4(1), 45-50.
Walsh T. (1994), The Binomial Theorem, Blue Book Note 903, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Walsh T. (1993), The Arithmetic/Geometric Mean Theorem, Blue Book Note 828, University of Edinburgh, Mathematical Reasoning Group (Edinburgh, United Kingdom).
Walther C. (1994), Mathematical Induction, Gabbay D., Hogger C., Robinson J., Handbook of Logic in Artificial Intelligence and Logic Programming, 127-228, Oxford University Press.
Walther C. (1983), A Many-Sorted Calculus Based on Resolution and Paramodulation, Bundy A., Proceedings of the 8th International Joint Conference on Artificial Intelligence (Karlsruhe, Germany), 882-891.
Wang H. (1965), Formalization and Automatic Theorem-Proving, Kalenich W.A., Proceedings of the IFIP Congress (NEED), 51-58, Spartan Books.
Wang T-C. (1985), Designing Examples for Semantically Guided Hierarchical Deduction, Joshi A., Proceedings of the 9th International Joint Conference on Artificial Intelligence (Los Angeles, USA), 1201-1207.
Wang T-C., Bledsoe W.W. (1987), Hierarchical Deduction, Journal of Automated Reasoning 3(1), 35-77.
Weibel C. (1994), An Introduction to Homological Algebra, Cambridge University Press.
Weidenbach C. (2001), Combining Superposition, Sorts and Splitting, Robinson A., Voronkov A., Handbook of Automated Reasoning, 1965-2011, Elsevier Science.
Weidenbach C. (1993), Extending the Resolution Method with Sorts, Bajcsy R., Proceedings of the 13th International Joint Conference on Artificial Intelligence (Chambery, France), 60-65, Morgan Kaufmann.
Weidenbach C., Gaede B., Rock G. (1996), SPASS and FLOTTER, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 141-145, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.
Whitehead A.N., Russell B. (1927), Principia Mathematica, Cambridge United Press.
Whitesitt J.E. (1961), Boolean Algebra and Its Applications, Addison-Wesley.
Wick C., McCune W.W. (1989), Automated Reasoning about Elementary Point-Set Topology, Journal of Automated Reasoning 5, 239 - 255.
Wiedijk F. (2006), The Seventeen Provers of the World, Lecture Notes in Computer Science 3600, Springer-Verlag.
Willis N., Sloane P., MacHale D., Dispezio M., Smith K., Gardner M., Sole T., Marshall R. (2006), The World's Biggest Book of Brainteasers & Logic Puzzles, Kimble B., Sterling Publishing.
Wilson D.S., Loveland D.W. (1989), Incorporating Relevancy Testing in SATCHMO, CS-1989-24, Department of Computer Science, Duke University (Durham, USA).
Wilson G.A., Minker J. (1976), Resolution, Refinements, and Search Strategies: A Comparative Study, IEEE Transactions on Computers C-25(8), 782-801.
Winker S. (1990), Robbins Algebra: Conditions that make a Near-Boolean Algebra Boolean, Journal of Automated Reasoning 6(4), 465-489.
Winker S. (1982), Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions, Journal of the ACM 29(2), 273-284.
Winkler S., Moser G. (2018), MaedMax: A Maximal Ordered Completion Tool, Galmiche D., Schulz S., Sebastiani R., Proceedings of the 9th International Joint Conference on Automated Reasoning (Oxford, United Kingdom), 388-404, Lecture Notes in Computer Science 10900.
Wojciechowski M. (1997), Yoneda Embedding, Journal of Formalized Mathematics 6(3), 377-379.
Wojciechowski W.S., Wojcik A.S. (1983), Automated Design of Multi-valued Logic Circuits by Automated Theorem Proving Techniques, IEEE Transactions on Computers C-32(8), 785-798.
Wojcik A.S. (1983), Formal Design Verification of Digital Systems, Proceedings of the 20th Design Automation Conference.
Wolfram S. (2002), A New Kind of Science, Wolfram Media.
Woronowicz E. (1990), Relations Defined on Sets, Journal of Formalized Mathematics 1(1), 181-186.
Wos L. (2010), Deriving a Complex Formula from Simple Axioms, AAR Newsletter 088-2010-06.
Wos L. (1998), Automating the Search for Elegant Proofs, Journal of Automated Reasoning 21(2), 135-175.
Wos L. (1996), The Automation of Reasoning: An Experimenter's Notebook with OTTER Tutorial, Academic Press.
Wos L. (1996), The Power of Combining Resonance with Heat, Journal of Automated Reasoning 17(1), 23-81.
Wos L. (1996), OTTER and the Moufang Identity Problem, Journal of Automated Reasoning 17(2), 215-257.
Wos L. (1995), Searching for Circles of Pure Proofs, Journal of Automated Reasoning 15(3), 279-315.
Wos L. (1994), Challenge in Group Theory, AAR Newsletter 26, 3-5.
Wos L. (1994), Two Challenge Problems, AAR Newsletter 27, 9.
Wos L. (1993), The Kernel Strategy and Its Use for the Study of Combinatory Logic, Journal of Automated Reasoning 10(3), 287-344.
Wos L. (1992), An Opportunity to Test Your Skills, and the Power of Your Automated Reasoning Program, AAR Newsletter 21, 10-11.
Wos L. (1989), A Challenge Problem and a Recent Workshop, AAR Newsletter 13, 2-8.
Wos L. (1988), Automated Reasoning - 33 Basic Research Problems, Prentice-Hall.
Wos L. (1965), Unpublished Note, NEED, Argonne National Laboratory (Argonne, USA).
Wos L., McCune W.W. (1988), Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs, Lusk E., Overbeek R., Proceedings of the 9th International Conference on Automated Deduction (Argonne, USA), 714-729, Lecture Notes in Computer Science 310, Springer-Verlag.
Wos L., McCune W.W. (1988), Searching for a Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report, ANL-88-10, Argonne National Laboratory (Argonne, USA).
Wos L., Overbeek R., Lusk E.L., Boyle J. (1992), Automated Reasoning: Introduction and Applications, McGraw-Hill.
Wos L., Overbeek R., Lusk E.L., Boyle J. (1984), Automated Reasoning: Introduction and Applications, Prentice-Hall.
Wos L., Ulrich D., Fitelson B. (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.
Wos L., Winker S., McCune W.W., Overbeek R., Lusk E.L., Stevens R. (1990), Automated Reasoning Contributes to Mathemetics and Logic, Stickel M.E., Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany), 485-499, Lecture Notes in Artificial Intelligence 449, Springer-Verlag.
Wos L., Winker S., Veroff R., Smith B., Henschen L. (1983), Questions Concerning Possible Shortest Single Axioms in Equivalential Calculus: An Application of Automated Theorem Proving to infinite Domains, Notre Dame Journal of Formnal Logic 24(2), 205-223.
Wu C.H., Lee S.J. (2001), Parallelization of a Hyper-Linking-based Theorem Prover, Journal of Automated Reasoning 26(1), 67-106.
Wysocki M., Darmochwa{\l} A. (1990), Subsets of Topological Spaces, Journal of Formalized Mathematics 1(1), 231-237.
Ye Z., Chou S., Gao X. (2008), An Introduction to Java Geometry Expert, Sturm T., Zengler C., Proceedings of the 7th International Workshop on Automated Deduction in Geometry (Shanghai, China), 189-195, Lecture Notes in Computer Science 6301, Springer-Verlag.
Zeman J. (1973), Modal Logic, the Lewis-Modal Systems, Oxford University Press.
Zhang H. (1993), Automated Proofs of Equality Problems in Overbeek's Competition, Journal of Automated Reasoning 11(3), 333-351.
Zhang H., Hua X. (1992), Proving the Chinese Remainder Theorem by the Cover Set Induction, Kapur D., Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), 431-445, Lecture Notes in Artificial Intelligence 607, Springer-Verlag.
Zhang H., Kapur D., Krishnamoorthy M. (1988), A Mechanizable Induction Principle for Equational Specifications, Lusk E., Overbeek R., Proceedings of the 9th International Conference on Automated Deduction (Argonne, USA), 152-181, Lecture Notes in Computer Science 310, Springer-Verlag.
Zhang J. (2005), Computer Search for Counterexamples to Wilkie's Identity, Nieuwenhuis R., Proceedings of the 20th International Conference on Automated Deduction (Tallinn, Estonia), 441-451, Lecture Notes in Artificial Intelligence 3632, Springer-Verlag.
Zhang J. (2000), Test Problem and Perl Scripts for Finite Model Searching, Association for Automated Reasoning Newsletter.
Zhang J. (1998), Showing the Independence of An Axiom for Temporal Intervals by Model Generation, AAR Newsletter 40.
Zhang J. (1994), Solution to Another Open Question in Combinatory Logic, AAR Newsletter 25, 8-10.
Zhang J. (1992), Solution to an Open Question in Combinatory Logic, AAR Newsletter 21, 12.
Zhang X. (2008), Using LEO-II to Prove Properties of an Explicit Substitution M-set Model, MSc thesis, Saarland University (Saarbruecken, Germany).
Zhang Y., Sutcliffe G. (2005), Lemma Management Techniques for Automated Theorem Proving, Konev B., Schulz S., Proceedings of the 5th International Workshop on the Implementation of Logics (Montevideo, Uruguay), 87-94.
Zukowski S. (1990), Introduction to Lattice Theory, Journal of Formalized Mathematics 1(1), 215-222.
{\L}ukasiewicz J. (1963), Elements of Mathematical Logic, Pergamon Press.
{\L}ukasiewicz J. (1948), The Shortest Axiom of the Implicational Calculus of Propositions, Proceedings of the Royal Irish Academy 52(3), 25-33.