A comprehensive framework for saturation theorem proving

DOI10.1007/978-3-030-51074-9_18MaRDI QIDQ5918558zbMATH OpenOpenAlexFDO

Authors Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Christian Blanchette

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-51074-9_18

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A comprehensive framework for saturation theorem proving
• Formal verification of a generic framework to synthesize SAT-provers
• Canonicity!
• scientific article; zbMATH DE number 1552532
• Abstract canonical inference

Cites work

• A combinator-based superposition calculus for higher-order logic
• A comprehensive framework for saturation theorem proving
• AVATAR: The Architecture for First-Order Theorem Provers
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Combining superposition, sorts and splitting
• Concrete semantics. With Isabelle/HOL
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 517065 (Why is no real title available?)
• scientific article; zbMATH DE number 2090321 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Labelled splitting
• Locales: a module system for mathematical theories
• On restrictions of ordered paramodulation with simplification
• Refutational theorem proving for hierarchic first-order theories
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Superposition for -free higher-order logic
• Superposition with datatypes and codatatypes
• Superposition with lambdas
• Theorem proving with ordering and equality constrained clauses
• Truly modular (co)datatypes for Isabelle/HOL

Cited in

(24)

• A unifying splitting framework
• Superposition with first-class booleans and inprocessing clausification
• Superposition for full higher-order logic
• Set of support, demodulation, paramodulation: a historical perspective
• Ground joinability and connectedness in the superposition calculus
• SCL(EQ): SCL for first-order logic with equality
• Reducing higher-order theorem proving to a sequence of SAT problems
• Satallax: An Automatic Higher-Order Prover
• Superposition for lambda-free higher-order logic
• Implementing Superposition in iProver (System Description)
• Testing a saturation-based theorem prover: experiences and challenges
• SAT-Inspired Eliminations for Superposition
• Superposition with lambdas
• A comprehensive framework for saturation theorem proving
• Making higher-order superposition work
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• A comprehensive framework for saturation theorem proving
• Unifying splitting
• SCL(EQ): SCL for first-order logic with equality
• Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
• Superposition for higher-order logic
• Superposition with Delayed Unification
• Verified Given Clause Procedures
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

Describes a project that uses

Uses Software

• Isabelle/HOL
• E Theorem Prover
• AVATAR
• Ordered_Resolution_Prover
• Waldmeister
• OTTER
• DISCOUNT
• Archive Formal Proofs
• VAMPIRE
• Locales

This page was built for publication: A comprehensive framework for saturation theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5918558)