SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions

DOI10.1007/978-3-540-79719-7_20MaRDI QIDQ3502709zbMATH OpenOpenAlexFDO

Authors Maarten Mariën, Johan Wittocx, Marc Denecker, Maurice Bruynooghe

Publication date 27 May 2008

Published in Theory and Applications of Satisfiability Testing – SAT 2008 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-79719-7_20

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• A decision procedure for satisfiability in separation logic with inductive predicates
• SAT-based proof search in intermediate propositional logics
• Integrating Inductive Definitions in SAT
• Logic Programming
• Efficient SAT-based proof search in intuitionistic propositional logic
• scientific article; zbMATH DE number 1222558
• Induction in saturation-based proof search
• Extending the reach of SAT with many-valued logics
• scientific article; zbMATH DE number 1302017
• Satisfiability calculus: an abstract formulation of semantic proof systems

Cites work

• A machine program for theorem-proving
• ASSAT: computing answer sets of a logic program by SAT solvers
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 1696828 (Why is no real title available?)
• scientific article; zbMATH DE number 1368933 (Why is no real title available?)
• Integrating Inductive Definitions in SAT
• Logic Programming
• Logic Programming and Nonmonotonic Reasoning
• Logic Programming and Nonmonotonic Reasoning
• Predicate Introduction Under Stable and Well-Founded Semantics
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• The alternating fixpoint of logic programs with negation
• The well-founded semantics for general logic programs
• Theory and Applications of Satisfiability Testing
• Well-Founded Semantics and the Algebraic Theory of Non-monotone Inductive Definitions

Cited in

(17)

• Conflict-driven answer set solving: from theory to practice
• SAT solving for termination proofs with recursive path orders and dependency pairs
• On abstract modular inference systems and solvers
• Connecting first-order ASP and the logic FO(ID) through reducts
• Semiring-induced propositional logic: definition and basic algorithms
• A logic of fixpoint definitions
• A formal theory of justifications
• The Design of the Sixth Answer Set Programming Competition
• SAT modulo intuitionistic implications
• Integrating Inductive Definitions in SAT
• Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3
• Relating constraint answer set programming languages and algorithms
• An approximative inference method for solving \(\exists \forall \)SO satisfiability problems
• Debugging for Model Expansion
• Satisfiability Checking for PC(ID)
• Logic Programming
• Design and results of the Fifth Answer Set Programming Competition

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions

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