Extracting models from clause sets saturated under semantic refinements of the resolution rule |
| |
| Authors: | Nicolas Peltier |
| |
| Affiliation: | Centre National de la Recherche Scientifique, Laboratoire LEIBNIZ-IMAG, 46 Avenue Félix Viallet, 38031, Grenoble Cedex, France |
| |
| Abstract: | We present an algorithm that—given a set of clauses S saturated under some semantic refinements of the resolution calculus—automatically constructs a Herbrand model 
of S.
is represented by a set of atoms with equality and disequality constraints interpreted over the finite tree algebra, hence the problem of evaluating first-order formulae in
is decidable. |
| |
| Keywords: | Logic in computer science Automated deduction Automated model building Saturation-based methods |
| 本文献已被 ScienceDirect 等数据库收录！ |
