IRIS Institutional Research Information System - AIR Archivio Istituzionale della Ricerca

IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Milano.

AIR nasce in UNIMI nel 2006 con lo scopo di raccogliere, documentare e conservare le informazioni sulla produzione scientifica dell'Università degli Studi di Milano e costituisce di fatto l'Anagrafe della ricerca dell'Ateneo.

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 appropriate for constructively ascertaining 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.

Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic / C. Fiorentini, M. Ferrari. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 21:3(2020), pp. 22.1-22.47.

Powered by IRIS-about IRIS-Utilizzo dei cookie

 Copyright © 2021