Automated theorem proving by resolution in non-classical logics
From MaRDI portal
Publication:2385426
DOI10.1007/s10472-007-9051-8zbMath1130.03010OpenAlexW2133998496MaRDI QIDQ2385426
Publication date: 12 October 2007
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-007-9051-8
Related Items (8)
Distributive Lattice-Structured Ontologies ⋮ A first polynomial non-clausal class in many-valued logic ⋮ Relative annihilators in bounded commutative residuated lattices ⋮ Internal axioms for domain semirings ⋮ \(\mathcal{L}\)-fuzzy annihilators in residuated lattices ⋮ Modal Semirings Revisited ⋮ Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) ⋮ On the refutational completeness of signed binary resolution and hyperresolution
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
- A logic for reasoning with inconsistency
- Satisfiability in many-valued sentential logic is NP-complete
- An algebraic approach to non-classical logics
- Modal languages and bounded fragments of predicate logic
- A framework for automated reasoning in multiple-valued logics
- Resolution and model building in the infinite-valued calculus of Łukasiewicz
- Decidability by resolution for propositional modal logics
- Metamathematics of fuzzy logic
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- Tarskian set constraints
- Resolution-based theorem proving for many-valued logics
- Positive modal logic
- Duality for algebras of relevant logics
- Many-valued logic and mixed integer programming
- Finiteness in infinite-valued Łukasiewicz logic
- The semantics and proof theory of the logic of bunched implications
- The Relevance of Semantic Subtyping
- Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving
- Ordered chaining calculi for first-order theories of transitive relations
- A propositional calculus with denumerable matrix
- SYMMETRICAL HEYTING ALGEBRAS WITH OPERATORS
- Logics without the contraction rule
- Translation Methods for Non-Classical Logics: An Overview
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Short Conjunctive Normal Forms in Finitely Valued Logics
- Polynomial Time Uniform Word Problems
- Exploiting data dependencies in many-valued logics
- BI as an assertion language for mutable data structures
- KI 2003: Advances in Artificial Intelligence
This page was built for publication: Automated theorem proving by resolution in non-classical logics
