Robinson, J.A.


LOGLISP: an alternative to PROLOG

Classics

Proper names (i.e., individual constants, predicates, and operators) are represented as identifiers which begin with an uppercase letter or a special character such as, *, %,,,, or $. A term is either a logical variable, an individual constant, or an op*erator-operand combination represented as a dotted pair (F. S) whose head F is the operator and whose tail S is the operand. It is also possible to place LOGLISP temporarily into a special input mode called the FACTS mode, in which successive assertions can be entered one after the other. Typing (PRINTFACTS) causes the entire knowledge base to be displayed, its assertions grouped into procedures.


Computational logic: the unification computation

Classics

In designing an actual realization of the unification algorithm the first question which arises is how best to represent the expressions in the computer store. We have a collection of tables: symbol, args, vble, arity, subst, term, equals, and part, each of which has the same number N of rows. All the tables have one column, with the exception of args; and args has as many columns as the arity of that symbol, in the expressions being represented, whose arity is largest. We always arrange matters so that in a normal representation, distinct rows represent distinct expressions, i.e., so that We are now ready to explain the computation.


A note on mechanizing higher order logic

Classics

It seems most unlikely that one could in general write purely applicative Schonfmkel descriptions', like (5), of functions already known to one in some other form. One makes assertions in the system by writing clauses, i.e., finite collections of literals considered as disjunctions of their members, universally quantified with respect to all variables. In other words, this is a first-order language in which there is only one relation symbol, namely equality; only one function symbol, namely application; and a collection of individual constants. In particular the resolution principle may be used as sole principle; or the resolution principle together with paramodulation (Robinson and Wos 1969); or Sibert's system (Sibert 1969); or the E-resolution system of Morris (1969).


The generalized resolution principle

Classics

The generalized resolution principle is a single inference principle which provides, by itself, a complete formulation of the quantifier-free first-order predicate calculus with equality. The completeness theory of the generalized resolution principle exploits the very intuitive and natural idea of attempting to construct counterexamples to the theorems for which proofs are wanted, and makes this the central concept. The expressions are all built up from primitive We shall usually employ lower case letters for individual symbols and upper case letters for function and relation symbols. Similarly, a counterexample to a general proposition is an interpretation which strongly satisfies its premisses but falsifies its conclusion.