Abstract
We present automated theorem provers implementing systems for intermediate logics, in the propositional and
first-order setting. They use an axiomatic embedding into intuitionistic logic based on cut-restricted sequent
calculi. All provers are evaluated on a large benchmark set of propositional and first-order formulas.
first-order setting. They use an axiomatic embedding into intuitionistic logic based on cut-restricted sequent
calculi. All provers are evaluated on a large benchmark set of propositional and first-order formulas.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics {(ARQNL} 2024) affiliated with the 12th International Joint Conference on Automated Reasoning {(IJCAR} 2024 |
| Editors | Christoph Benzmüller, Jens Otten, Revantha Ramanayake |
| Publisher | CEUR Workshop Proceedings (CEUR-WS.org) |
| Pages | 14-23 |
| Number of pages | 10 |
| Volume | 3875 |
| Publication status | Published - 1-Jul-2024 |
Fingerprint
Dive into the research topics of 'Implementing Intermediate Logics'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver