Title | ||
---|---|---|
Duality between unprovability and provability in forward proof-search 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. 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 which is prone to constructively ascertain the unprovability of a formula G by providing a concise countermodel for it; in particular we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as result of a failed proof-search in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal. |
Year | Venue | Field |
---|---|---|
2018 | arXiv: Logic | Discrete mathematics,Proof search,Automated theorem proving,Propositional calculus,Inverse method,Duality (optimization),Mathematics,Calculus |
DocType | Volume | Citations |
Journal | abs/1804.06689 | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Camillo Fiorentini | 1 | 121 | 21.00 |
Mauro Ferrari | 2 | 93 | 16.05 |