Induction and Skolemization in saturation theorem proving

&
Annals of Pure and Applied Logic 174 (1):103167 (2023)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2022.103167

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,497

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Symbolic logic and mechanical theorem proving.Chin-Liang Chang - 1973 - San Diego: Academic Press. Edited by Richard Char-Tung Lee.
Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings.Rajeev Gore, Alexander Leitsch & Tobias Nipkow - 2001 - Springer Verlag.
Automated Theorem-proving in Non-classical Logics.Paul B. Thistlewaite, Michael A. McRobbie & Robert K. Meyer - 1988 - Pitman Publishing.
Fermat’s Last Theorem Proved by Induction (and Accompanied by a Philosophical Comment).Vasil Penchev - 2020 - Metaphilosophy eJournal (Elsevier: SSRN) 12 (8):1-8.
Connection-driven inductive theorem proving.Christoph Kreitz & Brigitte Pientka - 2001 - Studia Logica 69 (2):293-326.
Inductive theorem proving based on tree grammars.Sebastian Eberhard & Stefan Hetzl - 2015 - Annals of Pure and Applied Logic 166 (6):665-700.
First-Order Logic and Automated Theorem Proving.Melvin Fitting - 1998 - Studia Logica 61 (2):300-302.
Proving Induction.Alexander Paseau - 2011 - Australasian Journal of Logic 10:1-17.
Theorem Proving in Higher Order Logics 11th International Conference, Tphols '98, Canberra, Australia, September 27-October 2, 1998 : Proceedings'.Jim Grundy & Malcolm Newey - 1998 - Springer Verlag.
A note on a theorem of Kanovei.Roman Kossak - 2004 - Archive for Mathematical Logic 43 (4):565-569.
A Recursion Planning Analysis of Inductive Completion.Richard Barnett, David A. Basin & Jane Hesketh - 1991 - Department of Artificial Intelligence, University of Edinburgh.
Theorem Proving in Higher Order Logics : Emerging Trends 11th International Conference, Tphols '98, Canberra, Australia, September 27-October 2, 1997 ; Supplementary Proceedings'.Jim Grundy & Malcolm Charles Newey - 1998
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.Michael J. C. Gordon & Tom F. Melham - 1993
Herbrand's theorem and term induction.Matthias Baaz & Georg Moser - 2006 - Archive for Mathematical Logic 45 (4):447-503.
Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove, UT, USA, September 11 - 14, 1995. Proceedings.E. Thomas Schubert, Phillip J. Windley, James Alves-Foss & International Workshop on Higher Order Logic Theorum Proving and its Applications - 1995 - Springer Verlag.

Analytics

Added to PP
2022-07-29

Downloads
8 (#1,325,033)

6 months
3 (#984,719)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Quantifier-free induction for lists.Stefan Hetzl & Jannik Vierling - forthcoming - Archive for Mathematical Logic:1-23.

Add more citations

References found in this work

On parameter free induction schemas.R. Kaye, J. Paris & C. Dimitracopoulos - 1988 - Journal of Symbolic Logic 53 (4):1082-1097.
A compact representation of proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
On the complexity of proof deskolemization.Matthias Baaz, Stefan Hetzl & Daniel Weller - 2012 - Journal of Symbolic Logic 77 (2):669-686.
A Computational Logic.Robert S. Boyer & J. Strother Moore - 1990 - Journal of Symbolic Logic 55 (3):1302-1304.

View all 10 references / Add more references