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)

Links

PhilArchive



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

External links

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

Through your library

Similar books and articles

Symbolic logic and mechanical theorem proving.Chin-Liang Chang - 1973 - San Diego: Academic Press. Edited by Richard Char-Tung Lee.
Inductive theorem proving based on tree grammars.Sebastian Eberhard & Stefan Hetzl - 2015 - Annals of Pure and Applied Logic 166 (6):665-700.
Proving Induction.Alexander Paseau - 2011 - Australasian Journal of Logic 10:1-17.
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.
Herbrand's theorem and term induction.Matthias Baaz & Georg Moser - 2006 - Archive for Mathematical Logic 45 (4):447-503.

Analytics

Added to PP
2022-07-29

Downloads
8 (#1,323,906)

6 months
3 (#984,149)

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