\( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality

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

zbMATH Keywords

equalitylattice-valued logic\( \alpha \)-equality axioms\( \alpha \)-GH paramodulation\( \alpha \)-paramodulation

Mathematics Subject Classification ID

Many-valued logic (03B50)

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)\)