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

DOI10.1016/J.IPL.2021.106167MaRDI QIDQ2234795zbMATH OpenOpenAlexWikidataFDO

Authors 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

classical propositional logicautomatic theorem provingtableauxminimum satisfiability problem

Mathematics Subject Classification ID

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

Recommendations

• A tableau calculus for non-clausal maximum satisfiability
• New tableau characterizations for non-clausal \textsc{MaxSAT} problem
• A Complete Calculus for Max-SAT
• A tableau calculus for minimal model reasoning
• Resolution for Max-SAT

Cites work

• scientific article; zbMATH DE number 1189106 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• A resolution calculus for MinSAT
• A tableau calculus for non-clausal maximum satisfiability
• Clause tableaux for maximum and minimum satisfiability
• On approximation algorithms for the minimum satisfiability problem
• On reducing maximum independent set to minimum satisfiability
• Optimizing with minimum satisfiability
• SAT and SMT technology for many-valued logics
• Simplification Rules for Intuitionistic Propositional Tableaux
• The Minimum Satisfiability Problem
• fCube: an efficient prover for intuitionistic propositional logic

Cited in

(3)

• The possibilistic Horn non-clausal knowledge bases
• A tableau calculus for non-clausal maximum satisfiability
• New tableau characterizations for non-clausal \textsc{MaxSAT} problem

Describes a project that uses

Uses Software

• fCube

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

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