Automated theorem proving by resolution in non-classical logics
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 4117898
- scientific article; zbMATH DE number 4092823
- scientific article; zbMATH DE number 1948187
- On the automatizability of resolution and related propositional proof systems
- Automated deduction by theory resolution
- scientific article; zbMATH DE number 2042611
- Automated theorem proving for Łukasiewicz logics
- scientific article; zbMATH DE number 1127072
- Automated theorem proving in temporal logic: \(T\)-resolution
- A resolution theorem prover for intuitionistic logic
Cites work
- scientific article; zbMATH DE number 3751028 (Why is no real title available?)
- scientific article; zbMATH DE number 3504935 (Why is no real title available?)
- scientific article; zbMATH DE number 559756 (Why is no real title available?)
- scientific article; zbMATH DE number 1735878 (Why is no real title available?)
- scientific article; zbMATH DE number 1028817 (Why is no real title available?)
- scientific article; zbMATH DE number 1950265 (Why is no real title available?)
- scientific article; zbMATH DE number 2042617 (Why is no real title available?)
- scientific article; zbMATH DE number 1489632 (Why is no real title available?)
- scientific article; zbMATH DE number 1775484 (Why is no real title available?)
- scientific article; zbMATH DE number 1775515 (Why is no real title available?)
- scientific article; zbMATH DE number 194916 (Why is no real title available?)
- scientific article; zbMATH DE number 1852925 (Why is no real title available?)
- scientific article; zbMATH DE number 1852927 (Why is no real title available?)
- scientific article; zbMATH DE number 1406811 (Why is no real title available?)
- A Kripke-style and relational semantics for logics based on Łukasiewicz algebras
- A framework for automated reasoning in multiple-valued logics
- A logic for reasoning with inconsistency
- A propositional calculus with denumerable matrix
- An algebraic approach to non-classical logics
- Automated deduction for many-valued logics
- BI as an assertion language for mutable data structures
- Decidability by resolution for propositional modal logics
- Duality for algebras of relevant logics
- Exploiting data dependencies in many-valued logics
- Finiteness in infinite-valued Łukasiewicz logic
- Herbrand's theorem for prenex Gödel logic and its consequences for theorem proving
- Logics without the contraction rule
- Many-valued logic and mixed integer programming
- Metamathematics of fuzzy logic
- Modal languages and bounded fragments of predicate logic
- Modal logic
- Ordered chaining calculi for first-order theories of transitive relations
- Polynomial Time Uniform Word Problems
- Positive modal logic
- Resolution and model building in the infinite-valued calculus of Łukasiewicz
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- Resolution-based theorem proving for many-valued logics
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- SYMMETRICAL HEYTING ALGEBRAS WITH OPERATORS
- Satisfiability in many-valued sentential logic is NP-complete
- Short Conjunctive Normal Forms in Finitely Valued Logics
- Tarskian set constraints
- The instance problem and the most specific concept in the description logic \(\mathcal{EL}\) w.r.t. terminological cycles with descriptive semantics
- The relevance of semantic subtyping
- The semantics and proof theory of the logic of bunched implications
- Translation Methods for Non-Classical Logics: An Overview
Cited in
(22)- scientific article; zbMATH DE number 1414298 (Why is no real title available?)
- scientific article; zbMATH DE number 4117898 (Why is no real title available?)
- Modal Semirings Revisited
- scientific article; zbMATH DE number 3871323 (Why is no real title available?)
- On the refutational completeness of signed binary resolution and hyperresolution
- Distributive lattice-structured ontologies
- scientific article; zbMATH DE number 1507196 (Why is no real title available?)
- Combining and automating classical and non-classical logics in classical higher-order logics
- Internal axioms for domain semirings
- \(\mathcal{L}\)-fuzzy annihilators in residuated lattices
- A resolution theorem prover for intuitionistic logic
- Automated theorem proving in temporal logic: \(T\)-resolution
- Relative annihilators in bounded commutative residuated lattices
- Resolution theorem proving
- Reasoning Support for Casl with Automated Theorem Proving Systems
- scientific article; zbMATH DE number 2042611 (Why is no real title available?)
- On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$
- Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\)
- A first polynomial non-clausal class in many-valued logic
- A case study in automated theorem proving: Finding sages in combinatory logic
- scientific article; zbMATH DE number 3989325 (Why is no real title available?)
- scientific article; zbMATH DE number 4061193 (Why is no real title available?)
This page was built for publication: Automated theorem proving by resolution in non-classical logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2385426)
