Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
The Inverse Method for the Logic of Bunched Implications
verfasst von : Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, Sungwoo Park
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. The Logic of Bunched Implications (
BI
), due to Pym and O’Hearn, is a logic which freely combines the familiar connectives of intuitionistic logic with multiplicative linear conjunction and its adjoint implication. We present the first formulation of an inverse method for propositional
BI
without units. We adapt the sequent calculus for
BI
into a forward calculus. The soundness and completeness of the calculus are proved, and a canonical form for bunches is given.