A Comprehensive Framework for Saturation Theorem Proving - Archive ouverte HAL Access content directly
Conference Papers Year : 2020

A Comprehensive Framework for Saturation Theorem Proving

(1, 2) , (1, 2) , (3) , (2, 4, 1, 5)
1
2
3
4
5

Abstract

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus, for instance within an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.
Fichier principal
Vignette du fichier
satur_paper.pdf (487.33 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03106208 , version 1 (11-01-2021)

Identifiers

Cite

Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. A Comprehensive Framework for Saturation Theorem Proving. IJCAR 2020 (Part I) International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.316-334, ⟨10.1007/978-3-030-51074-9_18⟩. ⟨hal-03106208⟩
60 View
87 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More