Paramodulation and Theorem-Proving in First-Order Theories with Equality
Paramodulation and Theorem-Proving in First-Order Theories with Equality
复制标题
一阶理论中的参调和定理证明
DOI：
10.1007/978-3-642-81955-1_19
复制
发表时间：
1983
期刊：
影响因子：
--
通讯作者：
L. Wos
中科院分区：
文献类型：
--
作者：
G. Robinson;L. Wos
一个项是一个单独的常数或变量或一个n-adic函数字母后跟n项。原子公式是一个n-adic谓词字母，后跟n项。文字是原子公式或其否定。子句是一组文字，被认为是代表其成员的普遍量化的析取。有时区分空子句□（被视为一个子句）和“其他”空集合（如子句的空集合）在符号上是不一致的，即使所有这些空集合都是相同的集合论对象o。基础子句（术语，字面）是没有变量的子句。子句C'（literal，term）是另一个子句C（literal，term）的instance，如果C中的变量被将C转换为C'的项一致替换。
A term is an individual constant or variable or an n-adic function letter followed by n terms. An atomic formula is an n-adic predicate letter followed by n terms. A literal is an atomic formula or the negation thereof. A clause is a set of literals and is thought of as representing the universally-quantified disjunction of its members. It will sometimes be notationally convenient1 to distinguish between the empty clause □, viewed as a clause, and ‘other’ empty sets such as the empty set of clauses, even though all these empty sets are the same set-theoretic object o. A ground clause (term, literal) is one with no variables. A clause C’ (literal, term) is an instance of another clause C (literal, term) if there is a uniform replacement of the variables in C by terms that transform C into C’.