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

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

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