Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization

TL;DR

This paper introduces a novel combination of proof calculi techniques that preserve solutions and avoid Skolemization, aiming to enhance inductive theorem proving foundations.

Contribution

It presents a new integration of raising, explicit variable dependency, the liberalized delta-rule, and solution preservation for first-order deductive theorem proving.

Findings

Achieves solution preservation without Skolemization

Provides a foundation for inductive theorem proving

Combines multiple proof calculus techniques effectively

Abstract

We present a combination of raising, explicit variable dependency representation, the liberalized delta-rule, and preservation of solutions for first-order deductive theorem proving. Our main motivation is to provide the foundation for our work on inductive theorem proving, where the preservation of solutions is indispensable.