Computing witnesses using the SCAN algorithm

DOI10.1007/978-3-031-99984-0_27MaRDI QIDQ6869931zbMATH OpenFDO

Authors Fabian Achammer, Stefan Hetzl, Renate A. Schmidt

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_27

zbMATH Keywords

formula equationssaturation theorem provingSCAN algorithmsecond-order quantifier elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A fixed-point theorem for Horn formula equations
• A knowledge level account of forgetting
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Boolean unification - the story so far
• Boolean unification with predicates
• Computing circumscription revisited: A reduction algorithm
• Computing witnesses using the SCAN algorithm
• Das Auflösungsproblem in der Klassenlogik
• Das Auflösungsproblem in der Klassenlogik
• Forgetting concept and role symbols in \(\mathcal{ALCH}\)-ontologies
• Forgetting in answer set programming -- a survey
• Hierarchic superposition revisited
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 3501560 (Why is no real title available?)
• scientific article; zbMATH DE number 1337728 (Why is no real title available?)
• scientific article; zbMATH DE number 1007358 (Why is no real title available?)
• scientific article; zbMATH DE number 1421198 (Why is no real title available?)
• Interpolation and symbol elimination in Vampire
• Mechanised uniform interpolation for modal logics K, GL, and iSL
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• Refutational theorem proving for hierarchic first-order theories
• Relational and Kleene-Algebraic Methods in Computer Science
• Rough Sets and Current Trends in Computing
• Saturation-based uniform interpolation for multi-modal logics
• Second-order quantifier elimination. Foundations, computational aspects and applications
• Symbol elimination and applications to parametric entailment problems
• System description: GAPT 2.0
• The Boolean solution problem from the perspective of predicate logic
• Towards automating duality
• Unified correspondence
• Uniform interpolation of \(\mathcal{ALC}\)-ontologies using fixpoints
• Untersuchungen über das Eliminationsproblem der mathematischen Logik.
• Vorlesungen über die Algebra der Logik. (Exacte Logik). I.

Cited in

(1)

• Computing witnesses using the SCAN algorithm

This page was built for publication: Computing witnesses using the SCAN algorithm

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