\( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
From MaRDI portal
Publication:2156971
DOI10.1007/s00500-020-05136-8zbMath1491.03022OpenAlexW3042394741MaRDI QIDQ2156971
Yang Xu, Yingfang Li, Jun Liu, Xingxing He
Publication date: 21 July 2022
Published in: Soft Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00500-020-05136-8
equalitylattice-valued logic\( \alpha \)-equality axioms\( \alpha \)-GH paramodulation\( \alpha \)-paramodulation
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Paramodulation with non-monotonic orderings and simplification
- \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic
- A unified algorithm for finding \(k\)-IESFs in linguistic truth-valued lattice-valued propositional logic
- A framework for automated reasoning in multiple-valued logics
- Lattice-valued logic. An alternative approach to treat fuzziness and incomparability
- Basic paramodulation
- On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic
- Contradiction separation based dynamic multi-clause synergized automated deduction
- GRUNGE: a grand unified ATP challenge
- Machine learning for first-order theorem proving
- General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic
- On -satisfiability and its -lock resolution in a finite lattice-valued propositional logic
- Proving Theorems with the Modification Method
- The CADE-27 Automated theorem proving System Competition – CASC-27
- A Machine-Oriented Logic Based on the Resolution Principle
- \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\)
- \(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\)