Truthful Monadic Abstractions

Taus Brock-Nannestad, Carsten Schürmann

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


In intuitionistic sequent calculi, detecting that a sequent is unprovable is often used to direct proof search. This is for instance seen in backward chaining, where an unprovable subgoal means that the proof search must backtrack. In undecidable logics, however, proof search may continue indefinitely, finding neither a proof nor a disproof of a given subgoal.

In this paper we characterize a family of truth-preserving abstractions from intuitionistic first-order logic to the monadic fragment of classical first-order logic. Because they are truthful, these abstractions can be used to disprove sequents in intuitionistic first-order logic.
Original languageEnglish
Title of host publicationIJCAR'12 Proceedings of the 6th international joint conference on Automated Reasoning
Publication date2012
ISBN (Print)978-3-642-31364-6
Publication statusPublished - 2012
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Truthful Monadic Abstractions'. Together they form a unique fingerprint.

Cite this