About: A Comprehensive Framework for Saturation Theorem Proving

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: A Comprehensive Framework for Saturation Theorem Proving Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	A Comprehensive Framework for Saturation Theorem Proving
Creator	Blanchette, Jasmin Robillard, Simon Tourret, Sophie Waldmann, Uwe
Source	PMC
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 [Image: see text] loop. Our framework is mechanized in Isabelle/ [Image: see text] .
has issue date	2020-05-30(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51074-9_18
has license	no-cc
sha1sum (hex)	387f36c139dda4da19be3b65deeec4f85cedcbc8
schema:url	https://doi.org/10.1007/978-3-030-51074-9_18
resource representing a document's title	A Comprehensive Framework for Saturation Theorem Proving
has PubMed Central identifier	PMC7324260
schema:publication	Automated Reasoning
resource representing a document's body	covid:387f36c139dda4da19be3b65deeec4f85cedcbc8#body_text
is schema:about of	named entity 'STATIC' covid:arg/387f36c139dda4da19be3b65deeec4f85cedcbc8 named entity 'decision procedures' named entity 'subsumption' named entity 'indexed family' named entity 'modulo' named entity 'computing' named entity 'countably infinite' named entity 'n-ary' named entity 'Inf' named entity 'N 1' named entity 'first-order logic' named entity 'unifiers' named entity 'proof calculi' named entity 'vacuously' named entity 'subsumption' named entity 'partial ordering' named entity 'subsumption' named entity 'standard definition' named entity 'calculus' named entity 'N 1' named entity 'equivalence relation' named entity 'well-founded' named entity 'Lemma' named entity 'universally quantified' named entity 'entailment' named entity 'consequence relation' named entity 'calculus' named entity 'associativity' named entity 'Isabelle/HOL' named entity 'nonempty subset' named entity 'Waldmeister' named entity 'Lemma' named entity 'tuple' named entity 'calculus' named entity 'underlying calculus' named entity 'calculus' named entity 'subsumption' named entity 'consequence relation' named entity 'entailment' named entity 'theorem proving' named entity 'dynamic behavior' named entity 'subset' named entity 'subsumption' named entity 'first-order' named entity 'Inf' named entity 'subset' named entity 'entailment' named entity 'partial ordering' named entity 'logic' named entity 'calculus' named entity 'higher-order' named entity 'logic' named entity 'commutativity' named entity 'equational theory' named entity 'consequence relation' named entity 'higher-order' named entity 'well-founded' named entity 'Inf' named entity 'partial ordering' named entity 'Simpli' named entity 'first-order' named entity 'lemma' named entity 'partial ordering' named entity 'subsumption' named entity 'semantics' named entity 'calculus' named entity 'well-founded' named entity 'ground instance' named entity 'theorem proving' named entity 'higher-order' named entity 'entailment' named entity 'subsumption' named entity 'skolemization' named entity 'nonempty set' named entity 'calculus' named entity 'Inf' named entity 'N 2' named entity 'Inf' named entity 'heuristically'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2025 OpenLink Software