Tree-like Refutation Search and Model Elimination Method
Închide
Articolul precedent
Articolul urmator
679 0
SM ISO690:2012
LYALETSKI, Alexander. Tree-like Refutation Search and Model Elimination Method. In: Conference on Mathematical Foundations of Informatics, Ed. 2018, 2-6 iulie 2018, Chișinău. Chișinău: "VALINEX" SRL, 2018, pp. 134-148. ISBN 978‐9975‐4237‐7‐9.
EXPORT metadate:
Google Scholar
Crossref
CERIF

DataCite
Dublin Core
Conference on Mathematical Foundations of Informatics 2018
Conferința "Conference on Mathematical Foundations of Informatics"
2018, Chișinău, Moldova, 2-6 iulie 2018

Tree-like Refutation Search and Model Elimination Method


Pag. 134-148

Lyaletski Alexander
 
Institute of Mathematics and Computer Science ASM
 
 
Disponibil în IBN: 3 iulie 2018


Rezumat

Calculi of so-called literal trees are constructed for solving the problem of refutation search in classical first-order logic without equality. Their soundness and completeness are proved. The connection of one of these calculi with a certain modification of the model elimination method is established, which gives the possibility to prove the soundness and completeness of the both modification and model elimination method and better understand the operation scheme of the model elimination method.

Cuvinte-cheie
classical first-order logic, clause, model elimination method, literal tree, refutation, soundness,

résolution, calculus, inférence, completeness