A first polynomial non-clausal class in many-valued logic
From MaRDI portal
Publication:6083144
DOI10.1016/J.FSS.2022.10.008zbMath1522.03099arXiv2110.12901OpenAlexW3209981694MaRDI QIDQ6083144
Publication date: 31 October 2023
Published in: Fuzzy Sets and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2110.12901
theorem provingresolutionlogic programmingtractabilityHornDPLLnon-clausalsatisfiability testingregular many-valued logic
Fuzzy logic; logic of vagueness (03B52) Logic in artificial intelligence (68T27) Reasoning under uncertainty in the context of artificial intelligence (68T37) Logic in computer science (03B70)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Learning general constraints in CSP
- Possibilistic logic: a retrospective and prospective view
- Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings
- The Helly property and satisfiability of Boolean formulas defined on set families
- A solver for QBFs in negation normal form
- Completely non-clausal theorem proving
- Non-resolution theorem proving
- A linear-time algorithm for testing the truth of certain quantified Boolean formulas
- A framework for automated reasoning in multiple-valued logics
- An alternative proof method for possibilistic logic and its application to terminological logics
- On the complexity of entailment in propositional multivalued logics
- Non-clausal connection calculi for non-classical logics
- Resolution-based theorem proving for many-valued logics
- Nested expressions in logic programs
- A characterization of belief merging operators in the regular Horn fragment of signed logic
- Certification of nonclausal connection tableaux proofs
- New complexity results for Łukasiewicz logic
- Automated theorem proving by resolution in non-classical logics
- Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
- ABox abduction in the description logic \(\mathcal{ALC}\)
- Resolution procedures for multiple-valued optimization
- An algorithm for random signed 3-SAT with intervals
- Regular-SAT: A many-valued approach to solving combinatorial problems
- Logic programming with signs and annotations
- Mathematical Logic for Computer Science
- Dissolution
- Ordered chaining calculi for first-order theories of transitive relations
- Characterising equilibrium logic and nested logic programs: Reductions and complexity,
- Foundations of Rule-Based Query Answering
- Efficient Algorithms for Description Problems over Finite Totally Ordered Domains
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Theorem Proving via General Matings
- Simplification of many-valued logic formulas using anti-links
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Short Conjunctive Normal Forms in Finitely Valued Logics
- Inconsistency Management from the Standpoint of Possibilistic Logic
- Symbolic possibilistic logic: completeness and inference methods
- Increasing the efficiency of automated theorem proving
- Exploiting data dependencies in many-valued logics
- Subgoaling Techniques for Satisficing and Optimal Numeric Planning
- The Complexity of 3-Valued Łukasiewicz Rules
- Automated Reasoning
- Decomposable negation normal form
- Satisfiability Checking of Non-clausal Formulas Using General Matings
- On sentences which are true of direct unions of algebras
- The decision problem for some classes of sentences without quantifiers
- Principles and Practice of Constraint Programming – CP 2004
- Reductions for non-clausal theorem proving
This page was built for publication: A first polynomial non-clausal class in many-valued logic
