计算机数理逻辑-一阶逻辑-逻辑编程

Resolution was originally developed as a method for automatic theorem proving. Later, it was discovered that a restricted form of resolution can be used for programming a computation. This approach is called logic programming.

• A program is expressed as a set of clauses
• A query is expressed as an additional clause that can clash冲突 with one or more of the program clauses. The query is assumed to be the negation of result of the program. If a refutation succeeds, the query is not a logical consequence of the program, so its negation must be a logical consequence.

解析最初是作为一种自动定理证明的方法而开发的。后来，人们发现，一种受限制的决议形式可以用于计算的编程。这种方法被称为逻辑编程。

• 一个程序被表达为一组子句
• 一个查询被表达为一个额外的子句，可以与一个或多个程序子句发生冲突。查询被认为是对程序结果的否定。如果反驳成功，查询不是程序的逻辑结果，所以它的否定必须是一个逻辑结果

1. From Formulas in Logic to Logic Programming

program clauses

• 按我的理解就是霍恩子句

goal clause

• Suppose now that we have a set of program clauses and we want to prove that some formula:
  • $G_1\land{}…\land{}G_n$
• is a logical consequence of the set. This can be done by taking the negation of the formula:
  • $\lnot{}G_1\lor{}…\lor{}\lnot{}G_n$
• and refuting it by resolution with the program clauses

  The formula $¬ G_1∨⋯∨¬ G_n$ , called a goal clause, consists entirely of negative literals, so it can only clash on the single positive literal of a program clause