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

DOI10.1016/J.IPL.2021.106167zbMATH Open1482.68269OpenAlexW3183746973WikidataQ114014155 ScholiaQ114014155MaRDI QIDQ2234795FDOQ2234795

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

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

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)

Cites Work

• fCube: an efficient prover for intuitionistic propositional logic
• Title not available (Why is that?)
• On approximation algorithms for the minimum satisfiability problem
• The Minimum Satisfiability Problem
• Title not available (Why is that?)
• Optimizing with minimum satisfiability
• On reducing maximum independent set to minimum satisfiability
• Title not available (Why is that?)
• Simplification Rules for Intuitionistic Propositional Tableaux
• Clause tableaux for maximum and minimum satisfiability
• A tableau calculus for non-clausal maximum satisfiability
• A resolution calculus for MinSAT
• SAT and SMT technology for many-valued logics

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

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)