Integrating Inductive Definitions in SAT

DOI10.1007/978-3-540-75560-9_28MaRDI QIDQ3498482zbMATH OpenOpenAlexFDO

Authors Maarten Mariën, Johan Wittocx, Marc Denecker

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75560-9_28

Mathematics Subject Classification ID

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

Recommendations

• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
• Logic Programming
• Satisfiability Checking for PC(ID)
• Temporal induction by incremental SAT solving
• A logic of fixpoint definitions

Cites work

• scientific article; zbMATH DE number 4160107 (Why is no real title available?)
• scientific article; zbMATH DE number 1368933 (Why is no real title available?)
• ASSAT: computing answer sets of a logic program by SAT solvers
• Conflict-Driven Answer Set Enumeration
• Integrating Inductive Definitions in SAT
• Logic Programming
• Logic Programming and Nonmonotonic Reasoning
• Satisfiability Checking for PC(ID)
• The alternating fixpoint of logic programs with negation
• The well-founded semantics for general logic programs
• Theory and Applications of Satisfiability Testing
• Why are there so many loop formulas?

Cited in

(5)

• Satisfiability Checking for PC(ID)
• Integrating Inductive Definitions in SAT
• Compiling \(\mathrm{input}^\ast\) FO\((\cdot)\) inductive definitions into tabled prolog rules for IDP3
• Logic Programming
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions

Describes a project that uses

Uses Software

• ASSAT

This page was built for publication: Integrating Inductive Definitions in SAT

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