Paper Info
Title
A Forward Unprovability Calculus for Intuitionistic Propositional Logic.
Abstract
The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. This method has been successfully applied to a variety of logics. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability. From a derivation of G in FRJ(G) we can extract a Kripke countermodel for G. Since in forward methods sequents are not duplicated, the generated countermodels do not contain redundant worlds and are in general very concise.
Year
DOI
Venue
2017
10.1007/978-3-319-66902-1_7
Lecture Notes in Artificial Intelligence
Field
DocType
Volume
Automated theorem proving,Inverse method,Propositional calculus,Algorithm,Mathematics,Calculus
Conference
10501
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
11
2
Name
Order
Citations
PageRank
Camillo Fiorentini112121.00
Mauro Ferrari29316.05