A non-clausal tableau calculus for \textsc{MinSat}

DOI10.1016/j.ipl.2021.106167zbMath1482.68269OpenAlexW3183746973WikidataQ114014155 ScholiaQ114014155MaRDI QIDQ2234795

Guido Fiorino

Publication date: 19 October 2021

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2021.106167

zbMATH Keywords

tableauxclassical propositional logicautomatic theorem provingminimum satisfiability problem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Related Items (1)

The possibilistic Horn non-clausal knowledge bases

Uses Software

• fCube

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On approximation algorithms for the minimum satisfiability problem
• Optimizing with minimum satisfiability
• A tableau calculus for non-clausal maximum satisfiability
• Simplification Rules for Intuitionistic Propositional Tableaux
• On Reducing Maximum Independent Set to Minimum Satisfiability
• The Minimum Satisfiability Problem
• fCube: An Efficient Prover for Intuitionistic Propositional Logic
• Clause tableaux for maximum and minimum satisfiability
• A resolution calculus for MinSAT

This page was built for publication: A non-clausal tableau calculus for \textsc{MinSat}