The tableau-like system KE is generalized to intuitionistic propositional logic by means of labelled signed formulas and constraints between labels, mimicking the relational semantics. To improve on proof-search and exploiting the meaning of negation, we further endow the system with free-variables. The resulting system enjoys the subformula property and terminates, either with a proof or a finite countermodel, without any extra mechanism. Proof and countermodel search is guided by generalizations of traditional reasoning patterns.
Labelled KE for intuitionistic propositional logic
Baldi, P;
2026-01-01
Abstract
The tableau-like system KE is generalized to intuitionistic propositional logic by means of labelled signed formulas and constraints between labels, mimicking the relational semantics. To improve on proof-search and exploiting the meaning of negation, we further endow the system with free-variables. The resulting system enjoys the subformula property and terminates, either with a proof or a finite countermodel, without any extra mechanism. Proof and countermodel search is guided by generalizations of traditional reasoning patterns.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
