Luis Martínez-Falero

Automated deduction based on contradiction separation extends the binary resolution principle, offering a novel approach to deductive inference rules. Constructing standard contradictions is essential for its efficiency. This paper systematically investigates two new types of standard contradictions in propositional and first‐order logic, enriching the library of standard contradictions and enhancing its effectiveness. First, we define two types of standard contradictions: sign‐boundary contradictions and diagonal vacancy‐type contradictions. Next, we propose the corresponding construction methods and present their properties related to contradiction composition and literal addition. Furthermore, we explore the transformations between these two types of contradictions and analyze the conditions necessary to construct standard contradictions. Finally, we extend these findings to first‐order logic, demonstrating their applicability in more complex logical systems.

Automated reasoning issues are addressed for a finite lattice-valued propositional logic LnP(X) with truth-values in a finite lattice-valued logical algebraic structure—lattice implication algebra. We investigate extended strategies and rules from classical logic to LnP(X) to simplify the procedure in the semantic level for testing the satisfiability of formulas in LnP(X) at a certain truth-value level α (α-satisfiability) while keeping the role of truth constant formula played in LnP(X). We propose a lock resolution method at a certain truth-value level α (α-lock resolution) in LnP(X) and have proved its theorems of soundness and weak completeness, respectively. We provide more efficient resolution based automated reasoning in LnP(X) and key supports for α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.