AutoLog

A,C,U,V (rule)

A is the size of the antecedent of the rule, C is the size of the consequent, U is the number of antecedent variables, and V is total number of variables in the rule; existential=V-U.

U is the number of Lterm variables, and V is total number of variables in the modultor; existential=V-U.

A rewrite has form Lterm = Rterm. Any matched Lterm is replaced by corresponding instance of Rterm.

A rule is complex provided that the number of function applications in a consequent exceeds the numberof function applications in the antecedent. A rewrite is complex provided that the number of function applications in the Rterm exceeds the numberof function applications in the Lterm.

rule contains a free variable in the consequent of the rule which is not bound in the antecedent of the rule or, for a rewrite, there is a variable in the Rterm which did not occur in the Lterm.

All arguments are bound by matching a literal appearing to the left of the occurence of the functor.

the unique numerical index of a variable name 0,.. numbered left-to-right in the parsed input inference expression, used as reference in variable matching tables.

the unique numerical index of a named predicate or function symbol in the current theory. (Parametrized predicates or operator symbols also acquire an index which may be used for Analyzer bookkeeping reference.)

When parsed left-to-right, every parametric functor term in the antecedent literal is bound in a literal to the left of the given literal.

When matched left-to-right, every parametric functor term in the consequent literal is bound by matching a literal in the antecedent of the rule or is bound by matching a literal to the left of the given literal withing its surrounding conjunction.

Every antecedent rule literal and consequent rule literal is indexical.

A static input program rewrite is indexical provided its Lterm is a Functor that has no parametric variable (unnamed) functions as subterms (e.g., F(X) is not indexical, but f(X)(Y) is indexical), and the Rterm contains no variable which does not occur in the Lterm.

A dynamic consequent identity literal serves as a dynamic rewrite modulator provide it appears in the consequent of an indexical autolog rule. Such a ground identity becomes an active modulator when it is asserted to branch as a fact.

Every inference form (rule or rewrite) in the theory is indexical.

an array indexed by the literal arguments, that records whether the variables in its arguments are bound by occurrences of the same variables in literals to the left of the containing literal (within the same conjunction) of a rule. For a rewrite whose Lterm is a functor, the Lterm key is an array indicating which of the Lterm arguments is bound.

provides an array of indices determining the order in which to match literal/Lterm arguments (preferring to satisfy bound arguments before arguments with unbound variables).

On input either the functor is named or has parameterized form F(...), where F has no variables and any arguments are descent-recursively predicative.

A term is "byName" (-.byName()) provided it is defined at input using a named constant or it is part of an assertion to branch whiched is constructed using a named constant. byName predicate or operator (function) terms thus have a null parametric (.fnctr) field. For example, A rule literal like 'p(f(a),X,g(b))' in an input program is considered to be byName, wheras 'p(i)(f(j)(a),X,g(k)(b))' is parametric and not byName. A predicate or operator term which is byName is also predicative.

The AutologAnalyzer(AA) determines the search methods to be used for matching rule literal factors or left-terms of rewrites. Generally speaking, predicativity enhances indexing more than indexicality, and indexicality more that free impredicativity. AA reports the status of its analysis as an autolog development tool. Some of the quick definitions above may be too brief: See the Autolog Design Notebook for more detailed information and examples. (5/12/2022)