Proof Search in Classical Propositional Logic with Partial Proof Terms

doi:10.1007/978-3-031-99536-1_18

Proof Search in Classical Propositional Logic with Partial Proof Terms

2026-01-01

0

PRE

AI

J

José Espírito Santo *

A

Ana Catarina Sousa

DOI：10.1007/978-3-031-99536-1_18

Original

Original request for help

Save

Abstract

En 中文

Partial (i.e. unfinished) proofs can be represented by partial proof terms. These are proof terms expressing gaps in incomplete derivations with the help offormal sequents, that is, sequents occurring as proper components of the syntax of proof terms. Our previous paper applied this methodology to intuitionistic propositional logic, to show that focusing in sequent calculus corresponds to intercalation in bidirectional natural deduction. The main goal of this paper is to extend these results to classical logic, using the same methodology. We consider the focused sequent calculus LKT and a bidirectional natural deduction system with alternative conclusions, NKT. In the latter system the admissible typing rule for structural substitution is in fact an elimination rule for an implications which is an alternative conclusion.

Keywords:

Proof search

Partial proof term

Partial derivation

Proof state

Focusing

Intercalation

Classical propositional logic

Proof Search in Classical Propositional Logic with Partial Proof Terms

Abstract

Journal

Organization