Articolul precedent |
Articolul urmator |
732 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 | ||||||
|
||||||
Pag. 134-148 | ||||||
|
||||||
Descarcă PDF | ||||||
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 |
||||||
|