An assumption-based approach for solving the minimal S5-satisfiability problem

DOI10.1007/978-3-319-94205-6_1OpenAlexW2810892201MaRDI QIDQ1799062FDOQ1799062

Authors Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_1

zbMATH Keywords

modal logicminimisationincremental SATS5

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Modal logic (including the logic of norms) (03B45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Minimizing models for Tseitin-encoded SAT instances
• Modal Satisfiability via SMT Solving
• Computing minimal models modulo subset-simulation for modal logics
• Minimal sets on propositional formulae. Problems and reductions
• Constraint programming for modelling and solving modal satisfiability

Cited in

(2)

• Efficient SAT-based minimal model generation methods for modal logic S5
• Modal logic S5 satisfiability in answer set programming

Describes a project that uses

Uses Software

• MiniSat
• SCIP
• SPASS
• Sat4j
• E Theorem Prover
• Spartacus
• LMHS
• MSPASS
• InKreSAT

This page was built for publication: An assumption-based approach for solving the minimal S5-satisfiability problem

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