Truthful Monadic Abstractions

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

View graph of relations

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

ID: 37332955