Truthful Monadic Abstractions

Taus Brock-Nannestad; Carsten Schürmann

doi:10.1007/978-3-642-31365-3_10

Truthful Monadic Abstractions

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

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 language	English
Title of host publication	IJCAR'12 Proceedings of the 6th international joint conference on Automated Reasoning
Volume	7364
Publisher	Springer
Publication date	2012
Pages	97-110
ISBN (Print)	978-3-642-31364-6
DOIs	https://doi.org/10.1007/978-3-642-31365-3_10
Publication status	Published - 2012

Series	Lecture Notes in Computer Science
Volume	7364
ISSN	0302-9743

Keywords

Intuitionistic sequent calculi
Proof search
Unprovable sequents
Backward chaining
Monadic fragment

Access to Document

10.1007/978-3-642-31365-3_10

Cite this

@inproceedings{f15b8fdf0ec44040b0b07cde237b799c,

title = "Truthful Monadic Abstractions",

abstract = "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.",

keywords = "Intuitionistic sequent calculi, Proof search, Unprovable sequents, Backward chaining, Monadic fragment, Intuitionistic sequent calculi, Proof search, Unprovable sequents, Backward chaining, Monadic fragment",

author = "Taus Brock-Nannestad and Carsten Sch{\"u}rmann",

year = "2012",

doi = "10.1007/978-3-642-31365-3_10",

language = "English",

isbn = "978-3-642-31364-6",

volume = "7364",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "97--110",

booktitle = "IJCAR'12 Proceedings of the 6th international joint conference on Automated Reasoning",

address = "Germany",

}

Truthful Monadic Abstractions. / Brock-Nannestad, Taus; Schürmann, Carsten.
IJCAR'12 Proceedings of the 6th international joint conference on Automated Reasoning. Vol. 7364 Springer, 2012. p. 97-110 (Lecture Notes in Computer Science, Vol. 7364).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Truthful Monadic Abstractions

AU - Brock-Nannestad, Taus

AU - Schürmann, Carsten

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - Intuitionistic sequent calculi

KW - Proof search

KW - Unprovable sequents

KW - Backward chaining

KW - Monadic fragment

KW - Intuitionistic sequent calculi

KW - Proof search

KW - Unprovable sequents

KW - Backward chaining

KW - Monadic fragment

U2 - 10.1007/978-3-642-31365-3_10

DO - 10.1007/978-3-642-31365-3_10

M3 - Article in proceedings

SN - 978-3-642-31364-6

VL - 7364

T3 - Lecture Notes in Computer Science

SP - 97

EP - 110

BT - IJCAR'12 Proceedings of the 6th international joint conference on Automated Reasoning

PB - Springer

ER -

Truthful Monadic Abstractions

Abstract

Keywords

Access to Document

Fingerprint

Cite this