Adding Sorts to an Isabelle Formalization of Superposition
Open Access
- 8 January 2026
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 104-116
Abstract
No abstract availableFunding Information
- European Research Council (101083038)
This publication has 19 references indexed in Scilit:
- A Comprehensive Framework for Saturation Theorem ProvingJournal of Automated Reasoning, 2022
- A Polymorphic Vampire2020
- The Higher-Order Prover Leo-III2018
- First-Order Theorem Proving and Vampire2013
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism2013
- Sort It Out with Monotonicity2011
- SPASS Version 3.52009
- Certification of Termination Proofs Using CeTA2009
- Integrating Linear Arithmetic into Superposition CalculusLecture Notes in Computer Science, 2007
- On restrictions of ordered paramodulation with simplification1990