Did you know ... | Search Documentation: |

Glossary of Terms |

- HOME
- DOWNLOAD
- DOCUMENTATION
- TUTORIALS
- Beginner▶
- Advanced▶
- Web applications▶
- Semantic web▶
- Graphics▶
- Machine learning▶
- External collections▶
- For packagers▶

- COMMUNITY
- COMMERCIAL
- WIKI

- Documentation
- Reference manual
- Introduction
- Overview
- Initialising and Managing a Prolog Project
- Built-in Predicates
- SWI-Prolog extensions
- Modules
- Tabled execution (SLG resolution)
- Constraint Logic Programming
- CHR: Constraint Handling Rules
- Multithreaded applications
- Coroutining using Prolog engines
- Foreign Language Interface
- Using SWI-Prolog in your browser (WASM)
- Deploying applications
- Packs: community add-ons
- The SWI-Prolog library
- Hackers corner
- Compatibility with other Prolog dialects
- Glossary of Terms
- SWI-Prolog License Conditions and Tools
- Summary
- Bibliography

- Packages

- Reference manual

**anonymous [variable]**- The
variable
`_`

is called the anonymous variable. Multiple occurrences of`_`

in a single term are not shared. **arguments**- Arguments are terms
that appear in a compound term.
`A1`and`a2`are the first and second argument of the term`myterm(A1, a2)`

. **arity**- Argument count (= number of arguments) of a compound term.
**assert**- Add a clause to a predicate. Clauses can be added at either end of the clause-list of a predicate. See asserta/1 and assertz/1.
**atom**- Textual constant. Used as name for compound terms, to represent constants or text.
**backtracking**- Search process used by Prolog. If a predicate offers multiple clauses to solve a goal, they are tried one-by-one until one succeeds. If a subsequent part of the proof is not satisfied with the resulting variable binding, it may ask for an alternative solution (= binding of the variables), causing Prolog to reject the previously chosen clause and try the next one.
**binding [of a variable]**- Current value of the variable. See also backtracking and query.
**built-in [predicate]**- Predicate that is part of the Prolog system. Built-in predicates cannot be redefined by the user, unless this is overruled using redefine_system_predicate/1.
**body**- Part of a clause
behind the neck
operator (

).`:-`

**choice point**- A choice point represents a choice in the search for a solution. Choice points are created if multiple clauses match a query or using disjunction (;/2). On backtracking, the execution state of the most recent choice point is restored and search continues with the next alternative (i.e., next clause or second branch of ;/2).
**clause**- ‘Sentence’of a Prolog program. A clause
consists of a head
and
body separated by
the neck operator (

) or it is a fact. For example:`:-`

parent(X) :- father(X, _).

Expressed as “X is a parent if X is a father of someone” . See also variable and predicate.

**compile**- Process where a Prolog program is translated to a sequence of instructions. See also interpreted. SWI-Prolog always compiles your program before executing it.
**compound [term]**- Also called structure.
It consists of a name followed by
`N`arguments, each of which are terms.`N`is called the arity of the term. **context module**- If a term is referring to a predicate in a module, the context module is used to find the target module. The context module of a goal is the module in which the predicate is defined, unless this predicate is module transparent, in which case the context module is inherited from the parent goal. See also module_transparent/1 and meta-predicate.
**dcg**- Abbreviation for
**Definite Clause Grammar**. **det [determinism]**- Short for deterministic.
**determinism**- How many solutions a goal can provide. Values are‘nondet’(zero to infinite),‘multi’(one to infinite),‘det’(exactly one) and‘semidet’(zero or one).
**deterministic**- A predicate is deterministic if it succeeds exactly one time without leaving a choice point.
**dynamic [predicate]**- A dynamic predicate is a predicate to which clauses may be asserted and from which clauses may be retracted while the program is running. See also update view.
**exported [predicate]**- A predicate is said to be exported from a module if it appears in the public list. This implies that the predicate can be imported into another module to make it visible there. See also use_module/[1,2].
**fact**- Clause
without a body.
This is called a fact because, interpreted as logic, there is no
condition to be satisfied. The example below states
`john`

is a person.person(john).

**fail**- A goal is said to have failed if it could not be proven.
**float**- Computer's crippled representation of a real number. Represented as‘IEEE double’.
**foreign**- Computer code expressed in languages other than Prolog. SWI-Prolog can only cooperate directly with the C and C++ computer languages.
**functor**- Combination of name and arity
of a compound
term. The term
`foo(a, b, c)`

is said to be a term belonging to the functor foo/3 . foo/0 is used to refer to the atom`foo`

. **goal**- Question stated to the Prolog engine. A goal is either an atom or a compound term. A goal either succeeds, in which case the variables in the compound terms have a binding, or it fails if Prolog fails to prove it.
**hashing**- Indexing technique used for quick lookup.
**head**- Part of a clause
before the neck
operator (

). This is an atom or compound term.`:-`

**imported [predicate]**- A predicate is said to be imported into a module if it is defined in another module and made available in this module. See also chapter 6.
**indexing**- Indexing is a technique used to quickly select candidate clauses of a predicate for a specific goal. In most Prolog systems, indexing is done (only) on the first argument of the head. If this argument is instantiated to an atom, integer, float or compound term with functor, hashing is used to quickly select all clauses where the first argument may unify with the first argument of the goal. SWI-Prolog supports just-in-time and multi-argument indexing. See section 2.17.
**integer**- Whole number. On all implementations of SWI-Prolog integers are at least 64-bit signed values. When linked to the GNU GMP library, integer arithmetic is unbounded. See also current_prolog_flag/2, flags bounded, max_integer and min_integer.
**interpreted**- As opposed to compiled, interpreted means the Prolog system attempts to prove a goal by directly reading the clauses rather than executing instructions from an (abstract) instruction set that is not or only indirectly related to Prolog.
**instantiation [of an argument]**- To what extend a term is bound to a value. Typical levels are‘unbound’(a variable),‘ground’(term without variables) or‘partially bound’(term with embedded variables).
**meta-predicate**- A predicate that reasons about other predicates, either by calling them, (re)defining them or querying properties.
**mode [declaration]**- Declaration of an argument instantiation pattern for a predicate, often accompanied with a determinism.
**module**- Collection of predicates. Each module defines a name-space for predicates. built-in predicates are accessible from all modules. Predicates can be published (exported) and imported to make their definition available to other modules.
**module transparent [predicate]**- A predicate that does not change the context module. Sometimes also called a meta-predicate.
**multi [determinism]**- A predicate
is said to have determinism
multi if it generates at
*least*one answer. **multifile [predicate]**- Predicate for which the definition is distributed over multiple source files. See multifile/1.
**neck**- Operator (

) separating head from body in a clause.`:-`

**nondet**- Short for non deterministic.
**non deterministic**- A non deterministic predicate is a predicate that may fail or succeed any number of times.
**operator**- Symbol (atom)
that may be placed before its operand
(prefix), after its operand
(postfix) or between its two operands
(infix).
In Prolog, the expression

`a+b`

is exactly the same as the canonical term`+(a,b)`

. **operand**- Argument of an operator.
**precedence**- The priority
of an operator.
Operator precedence is used to interpret
`a+b*c`

as`+(a, *(b,c))`

. **predicate**- Collection of clauses with the same functor (name/arity). If a goal is proved, the system looks for a predicate with the same functor, then uses indexing to select candidate clauses and then tries these clauses one-by-one. See also backtracking.
**predicate indicator**- Term of the form Name/Arity
(traditional) or Name//Arity (ISO DCG proposal), where Name is an atom
and Arity a non-negative integer. It acts as an
*indicator*(or reference) to a predicate or DCG rule. **priority**- In the context of operators a synonym for precedence.
**program**- Collection of predicates.
**property**- Attribute of an object. SWI-Prolog defines
various
**_property*predicates to query the status of predicates, clauses. etc. **prove**- Process where Prolog attempts to prove a query using the available predicates.
**public list**- List of predicates exported from a module.
**query**- See goal.
**retract**- Remove a clause from a predicate. See also dynamic, update view and assert.
**semidet**- Shorthand for
**semi deterministic**- .
**semi deterministic**- A predicate that is semi deterministic either fails or succeeds exactly once without a choice point. See also deterministic.
**shared**- Two variables
are called shared
after they are unified.
This implies if either of them is bound,
the other is bound to the same value:
?- A = B, A = a. A = B, B = a.

**singleton [variable]**- Variable
appearing only one time in a clause.
SWI-Prolog normally warns for this to avoid you making spelling
mistakes. If a variable appears on purpose only once in a clause, write
it as
`_`

(see anonymous). Rules for naming a variable and avoiding a warning are given in section 2.15.1.10. **solution**- Bindings resulting from a successfully proven goal.
**structure**- Synonym for compound term.
**string**- Used for the following representations of text: a packed array (see section 5.2, SWI-Prolog specific), a list of character codes or a list of one-character atoms.
**succeed**- A goal is said to have succeeded if it has been proven.
**term**- Value in Prolog. A term is either a variable, atom, integer, float or compound term. In addition, SWI-Prolog also defines the type string.
**transparent**- See module transparent.
**unify**- Prolog process to make two terms equal by
assigning variables in one term to values at the corresponding location
of the other term. For example:
?- foo(a, B) = foo(A, b). A = a, B = b.

Unlike assignment (which does not exist in Prolog), unification is not directed.

**update view**- How Prolog behaves when a dynamic predicate is changed while it is running. There are two models. In most older Prolog systems the change becomes immediately visible to the goal, in modern systems including SWI-Prolog, the running goal is not affected. Only new goals ‘see’the new definition.
**variable**- A Prolog variable is a value that‘is
not yet bound’. After binding
a variable, it cannot be modified. Backtracking
to a point in the execution before the variable was bound will turn it
back into a variable:
?- A = b, A = c. false. ?- (A = b; true; A = c). A = b ; true ; A = c .

See also unify.

Most of the links on this page are broken. When I click on them, they lead to a "404 not found" page.

"A Prolog variable is a value that‘is not yet bound'."

That sound not correct (it would explain why var/1 is called var/1 and not unbound/1 though, but is in contradiction with all other usage of the word 'variable', in particular with the usage under "binding of a variable").

Better: A "variable" is a name (with clause scope) denoting a term or an empty cell. If it designates an empty cell, it is an unbound or uninstantiated variable, otherwise it is a bound variable, namely a variable bound to the term it denotes. The "binding state" of a variable may change from unbound to bound. Trivially:

var(X),X=1,nonvar(X)

which should really have been written

unbound(X),X=1,bound(X)

OTOH, there is a slight shift in the meaning of the word "variable" when used for a variable name in the head (where it is always unbound as it appears in unification) and in a goal (where its "bounded-ness/instantiated-ness status" changes from "fresh & unbound" to "still unbound" to "bound/partially bond" to "bound/ground").

In all these case, `X` is a "variable", but the meaning changes.

It is actually clearer to say that `X` is a variable name and denotes en empty cell ("X is an unbound variable") or a (proper? nonempty?) term. (apparently an empty cell is also a "term")

f(X) :- atomic(X),!,h0(X). % at !, we know that variable X denotes an atomic term f(X) :- ground(X),!,h1(X). % at !, we know that variable X denotes a ground term f(X) :- nonvar(X),!,h2(X). % at !, we know that variable X does not denote an empty cell ("is not an unbound variable") f(X) :- var(X),!,h3(X). % at !, we know that variable X is unbound

Some adapted from

- "Deduction Systems", Rolf Socher-Ambrosius, Patricia Johann, Springer 1997
- "Memoing for Logic Programs", David S. Warrne, CACM Marc 1992 (Vol.35 No.3)
- Deduction/Induction/Abduction from "Abductive reasoning in Prolog and CHR" (Henning Christiansen, 2005)
- "typein module" as used on the page operators: the module into which code typed in at the toplevel (using the
`[user]`

prompt) is added (I suppose).

See here: https://eu.swi-prolog.org/pldoc/man?section=preddesc

**Comma-list**(as used on the page for tabling): A list constructed with functor `,/2`, which is not a real list as it terminates in a list element:`(1,2,3) = (1,(2,3))`

. Generally used as a conjunction.**Character**or**Char**is an atom of length 1. Prolog has no specific character type.**Predicate Activation**or just**Activation**: Basically, the stack frame of the predicate call. The runtime context of a clause in which variables denote concrete values (terms or empty cells). Corresponds to a "Byrd Box".**Unbound variable**vs.**Unbound value**: An**unbound variable**is a variable name that denotes an "empty cell" in memory. It is a variable name for which var/1 exactly succeeds at call time (but maybe not later, after a unification occurs. On the other hand, definitely earlier because you cannot "unbind" a variable except through backtracking; this is waht i means for Prolog to be "assign-once"). An**unbound value**is a position in a complex term that denotes an "empty cell" in memory but that does not have a name. For example:`length(L,2)`

.`L`is an unbound variable at first that is then unified with a complex term (a list of length 2) with 2 unbound values, which, when printed, appear as 2 unbound variables (i.e. their arbitrarilly chosen names are printed rather than their nonexistent content):`L = [_5038, _5044]`

.)- Predicate
**well-behavedness** - Predicate
**steadfastness**. A more general definition: In "The Craft of Prolog" Richard O’Keef writes on page 96 that "we call the property of refusing to give wrong answers even when the query has an unexpected form (typically supplying values for what we normally think of as inputs*) steadfastness". Note that the ISO standard says nothing about this concept, although built-in predicates are generally "steadfast". **Partial term / Partially ground term**: That term that is an unbound variable or may contain unbound variables not 100%% sure whether an unbound variable actually counts as such; the mode indicator descriptions seem to imply no).**Floundering**: When negation-as-failure pretzels itself and leads to wrong answers because the negated goal contains unbound variables (i.e. is nonground). Raymond Reiter writes in "Knowledge in Action" (MIT Press, 2001): "Eclipse Prolog provides two negation operators, one of which suspends itself on negative, non-ground atoms, hoping that their free variables will eventually become bound during the rest of the computation, at which point the operator resumes."**Closure**(in the Prolog sense) (from the page for`library(yall)`

: The closure concept used here is somewhat different from the closure concept from functional programming. The latter is a function that is always evaluated in the context that existed at function creation time. Here, a closure is a term of arity 0 =< L =< K. The term's name is the name of a predicate of arity K and the term's L arguments (where L could be 0) correspond to L leftmost arguments of said predicate. The remaining K-L arguments are left open and will be filled in by at metacall time. For example, a closure involving atom_concat/3 might be the term`atom_concat(prefix)`

. In order of increasing L, one would have increasingly more complete closures that could be passed to call/3, all giving the same result:`call(atom_concat,prefix,suffix,R)`

.`call(atom_concat(prefix),suffix,R)`

.`call(atom_concat(prefix,suffix),R)`

.`call(atom_concat(prefix,suffix,R))`

.

**Fresh variable**- a Prolog variable name that has not been used "to the left" and denotes a newly allocated "empty cell" in memory. For example,`_`is always fresh where it appears.**Iterative Deepening**- a heuristic to expand search trees which can be used in particular to transform Prolog's depth-first search strategy into a depth-limited breadth-first search strategy. This expands shallow nodes first and avoids accidental infinite descent on depth-first search. See "Depth-First Iterative Deepening: An Optimal Admissible Tree Search" by Richard Korf, Artificial Intelligence 27 (1985), Elsevier. Also Wikipedia. See also call_with_depth_limit/3 and call_with_inference_limit/3**Guard**- a test made at the beginning of a clause body for conditions that cannot be captured by simple head unification. Often followed by a cut to "commit" to the clause. Generally done using `,/2` but sometimes using ->/2. Example:

choo(X) :- var(X) -> (!,debug(choo,"It's a var",[])). choo(X) :- nonvar(X) -> debug(choo,"It's not a var",[]).

**Guarded Horn Clauses**,**Guarded Definite Clauses**particular logic programming languages derived from Prolog meant to be run on (highly) parallel machines (in particular so-called "5th generation" hardware). This research branch seems to have been abandoned (for now). Languages like**PARLOG**and**Parallel Prolog**are ancestors. See also: The deevolution of concurrent logic programming languages.**CHR**- Abbreviation for**Constraint Handling Rules**, an approach promoting forward-chaining rules working on a blackboard store. SWI-Prolog has an implementation running in the context of a single clause: CHR. See also: Wikipedia: Constraint Handling Rules**Clause indexing**- how a Prolog implementation looks up a matching clause head. Indexing may or may not be done on several arguments. SWI-Prolog indexes on first argument only, so if you want high discrimination by cases, move the most discriminatory parameter to the first place.**Clean/Defaulty representation**- a question of coding style. Clean representations can be efficiently distinguished by head unification alone. Defaulty (a pun on "faulty") representations force a coding style where a clause head matches, and the body distinguishes. This may be inefficient at runtime. See Triska's Triska's discussion at Clean vs. defaulty representations.**Cell**A memory location. It is either*empty*or holds an*atomic term*or a*compound term*which referencing other cell containing the compound term name and the compound term arguments. A special case is the**list cell**with name `[|]` and two arguments (i.e. with arity 2). In LISP, this is called the "consbox", with the first argument the "car" and the second the "cdr". Once a cell has been filled, it becomes indistinguishable from other cells with the same content (`my_atom`

==`my_atom`

) or at the root of graphs of cells forming ground terms (`f(g(a,b),c)`

==`f(g(a,b),c)`

). This allows the underlying machinery to share parts of graphs representing terms. In a Prolog program, a cell, or rather, the root of graph of cells is denoted by a variable (`X = f(g(a,b),c)`

). Thinking in terms of cells instead of terms is generally not needed unless empty cells and non-logical usage thereof enters the picture.**List cell**a cell holding the compound term `[|]` (in SWI-Prolog, traditionally `.` in other Prologs) and two arguments. In a well-constructed list the, there is a list element on argument position 1 and there is a next listcell of the list backbone or`[]`

on element position 2.**Empty cell**a cell holding (as yet) nothing but which may be set to an atomic value of the root of a graph of cells as computation progresses. Setting an empty cell can be done only once (Prolog is "assign-once") but can be rolled back on backtracking. Empty cells are denoted by initially fresh variables in a Prolog clause. Non-atomic terms, which are roots of trees and sometimes graphs of cells, can have empty cells at their leaves nodes. Unlike ground terms, empty cells are distinguishable and have identity:`X \== Y.`

: what these fresh variables denote, which are empty cells, are not the same, but`X=a,Y=a,X==Y.`

. Empty cells are merged via unification:`X \==Y, X=Y, X == Y`

:`X`and`Y`now designate the same empty cell. Thinking in terms of empty cells is not logical but computational and stateful in nature, and is done in the parts of the Prolog program which are doing state manipulation, for example those dealing with difference lists of open lists.**Empty cell attributes**: Empty cells can have named or unnamed**attributes**. There is no common notation for those, and they are never printed out as such. In other words, "unbound variables can carry attributes". Attributes may denote goals to be called as coroutines when the empty cell participates in a unification (is made non-empty or is merged with another empty cell). Colloquially "when the variable is bound". If that goal fails, the unification fails. This allows one to increase the power of unification, even in when used in a clause head.- freeze/2 and family:
`freeze(X,write("Hello")),X=1.`

prints`Hello`. - dif/2 (ensure two variables are always different) and family:
`dif(X,Y),X=1,Y=2.`

succeeds but`dif(X,Y),X=1,Y=1.`

fails **Attributed variables**: A generalization which allows the programmer to set/get arbitrary attributes on an empty cell and perform arbitrary decisions on unifications.

- freeze/2 and family:
**Linting**: The process of checking Prolog code for style errors and dubious constructions prior to compilation. This is done by`library(check)`

and`library(codewalk)`

. See also`library(prolog_xref)`

See also the Wikipedia entry on the`lint`

program**Pure Prolog**: Unclear, depends on opinion. A Prolog that only allows Horn clauses, without control-flow constructs like !, ->, no negation-as-failure \+ (but presumably still allows \= as the FOL "not equal"), possibly no meta-predicates incl. "call", which may possibly terminate independently of clause ordering. A Prolof which is "nearer" an ideal fragment of First-Order Logic.**Proper Prolog**: A proper Prolog interpreter is one that evaluates a negative literal not A, using negation-as-failure, and moreover, does so only when (at the time of evaluation) the atom A is ground. When A is not ground, the interpreter may suspend its evaluation, working on other literals until (with luck) A does become ground, or it may abort its computation. Either way, it never tries to fail on non-ground atoms. (Directly copied from Raymond Reiter: "Knowledge in Action", MIT Press, 2001 p. 107)

**Definite logic program**or**Positive logic program**or**Horn logic program**: A logic program consisting of clauses of the form `a_0 :- a_1, .... , a_m (i.e. Prolog programs without negation)**Normal logic program**or**General logic program**: A logic program consisting of clauses of the form `a_0 :- a_1, .... , a_m, \+ a_{m+1}, ... \+ a_n.`, where`\+`

stands for negation-as-failure. (i.e. Prolog program with negation)**Extended logic program**: A logic program consisting of clauses of the form `l0 :- l_1, .... , l_m, \+ l_{m+1}, ... \+ l_n.`, where l0 ... ln denote literals formed by means of strong negation l = a or l = ¬a. (**Not**supported in Prolog)**Positive disjunctive logic program**: A logic program consisting of non-Horn clauses of the form `a_0 ⋁ ... ⋁ a_n :- b1_1, .... , b_m (i.e. disjunctions are allowed in the head, making formulation of "uncertain knowledge" feasible;**not**supported in Prolog)

**Deduction**, reasoning within the knowledge we already have, i.e. from those facts we know and those rules and regularities of the world that we are familiar with. E.g. reasoning from causes to effects: _"If you make a fire here, you will burn down the house."_ (Henning). To a first approximation, Prolog performs reverse deduction, aka. goal-directed search: _"To burn down the house, make a fire here"_, but in relatively basic and "programming" context. To apply this to actual planning and commonsense reasoning you need to have a more extensive logical infrastructure than Prolog provides out of the box. See for example Event Calculus.**Induction**, finding general rules from the regularities that we have experienced in the facts that we know: these rules can be used later for prediction: _"Every time I made a fire in my living room, the house burnt down, aha, ... the next time I make a fire in my living room, the house will burn down, too."- (Henning) This is the purview of (unsupervised and symbol-based) machine learning. See Inductive Logic Programming for on introduction on how logic programming can be used in this domain.**Abduction**, reasoning from observed results to the basic fact from which they follow, quite often it means from an observed effect to produce a qualified guess for a possible cause: _"The house burnt down, perhaps my cousin has made a fire in the living room again."_ The corresponding formalization and extension for logic programming is the subject of Abductive Logic Programming**Deductive database**: Database implemented through a logic program that allows no function symbols and thus is based on a finite universe. Datalog is the paradigm here. (For a deductive database connected to a LISP-like language: datomic). (How does this compare to a relational database with recursive operations / fixpoint operations? Should be the same...)**Extensional database (EDB)**: The part of a logic program (or deductive database) that consist in facts.**Intensional database (IDB)**: The part of a logic program (or deductive database) that consists in rules (implications and integrity constraints). In a deductive database, EDB+IDB form a compressed representation of all the ground atoms that can be*deduced*going bottom-up chaining implications "forward" from premiss to conclusion to conclusion until a fixpoint of the ground atoms has been reached. When doing a proof "top-down", one is verifying whether an atom is indeed a member of that fixpoint.**Herbrand Universe**: The set of all ground terms constructed from constants and function symbols that appear in the program.**Herbrand Base**: The set of all ground atoms ("atoms" in the logical sense, i.e. predicate calls, not in the Prolog sense of "distinguishable identifiers/strings") that can be constructed from predicate symbols that appear in the program and terms from the Herbrand Universe.**Proof witness**or**proof solution**: a set of ground or partially ground terms that form a solution to a query with unbound variables:`length([1,2],L)`

, gives`L=2`

; the`2`

is the proof witness (the proof is "constructive" and doesn't just say true or false). Sometimes Prolog emits a "template proof witness" instead:`length(List,2)`

gives`List=[_,_]`

, which is really a (most general) template for lists of length 2.**Free variable**- this is sometimes used in the sense of a variable that is unbound (in the Prolog sense: it has no value). That's confusing though. In logic, the "free variable" in a formula is one which is not bound (in the logic sense) by a quantifier (or a lambda if those are allowed). A bound variable is said to be "in the scope of a quantifier". The same variable (variable name) can occur in a formula in places where it is bound and free, so we have to really talk about free and bound*occurrences*of variables rather than free and bound variables.**Theory**- A set of true sentences (expressed in and part of some specified logic). Concretely, a Prolog program*is*a theory with facts and sentences pre-labeled as "true".**Model Theory**: In mathematics, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models, taken as interpretations that satisfy the sentences of that theory.**Proof Theory**: Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.**Model**- A truth value assignment to atoms (i.e. facts) that makes all of the sentences of a theory true (and doesn't imply inconsistencies).**Sentence**- A formula in which no variable occurs free, also a**closed formula**. A formula containing at least one free occurrence of a variable is**open**(Socher-Ambrosius). See also: Wikipedia: Sentence): "a Boolean-valued well-formed formula with no free variables." Given a logic, a sentence is:**Valid**: : If the sentence is true in all models.**Satisfiable**: If there is at least one model in which the sentence is true.**Unsatisfiable**: If there is no model in which the sentence is true.

**Statement**- "A sentence put to work". From Wikipedia: Statement: (a) a meaningful declarative sentence that is true or false, or (b) the assertion that is made by a true or false declarative sentence. In some treatments "statement" is introduced in order to distinguish a sentence from its informational content. A statement is regarded as the information content of an information-bearing sentence. Thus, a sentence is related to the statement it bears like a numeral to the number it refers to. Statements are abstract logical entities, while sentences are grammatical entities.**Expression**- From Wikipedia: Expression: In mathematics, an expression or mathematical expression is a finite combination of symbols that is well-formed according to rules that depend on the context.**Proposition**- More or less the same as a Statement or a Sentence. See Wikipedia: Proposition. In**propositional logic**, we do not work at level of expressions involving relations and objects and equality and quantifiers but at the level of (opaque) propositional variables linked by logic operators; the propositional variables takes one a value from some finite set (generally a value of the finite set {true,false}; but one can generalize to non-logic settings, for example in belief networks the propositional variable can take on any of a set of values describing an outcome and logical connectives take on the meaning of set operations)**Theorem**- A sentence (of some logic adjoined to some theory) that can be labeled true ("proven") by a proof procedure. Goals for which the Prolog prover succeeds (which the Prolog prover accepts) are theorems for the pair (Prolog logic,Prolog program). A theorem is of course accompanied by at least one proof. Note that most Theorems are of low interest: for example, in the theory of Peano Numbers,`1+2<4`

. See also: Wikipedia: Theorem, which has a glossary of related terms (Corollary etc.). That page also cites Paul Hoffman as _"It has been estimated that over a quarter of a million theorems are proved every year."_ Well, with Prolog you can prove a million theorems in a minute!**Tautology**- A sentence (of some logic adjoined to some theory) that is true in all models. For example, in classical propositional logic: `(A ⇒ B) ⇔ (¬A ∨ B)` See also: Wikipedia: Tautology.**Signature**of a logic, Sigma = `<F,P>`, is a set of function symbols name/arity adjoined to a set of predicate symbols name/arity**Atom (logic)**(not to be confused with the "atom" of Prolog), or "atomic formula" is a word`p(t1,...,tn)`

, n>=1 where`p`

is a predicate symbol from a set`P`and the`ti`

are terms from `T(F,V)`, build from a set of function symbols`F`and variable symbols from set of variable symbols`V`. The atom can also be a word of the form`s = t`

where`s`

,`t`

`T(F,V)`. The set of atoms may be written `A(F,P)` (note that 0-arity predicate symbols are in principle not allowed)**Literal**either an atom (a "positive literal") or its negation (a "negative literal") appearing in a formula. In Prolog, there is some subtlety involved with the fact that the negation is "weak" in the sense that it expresses negation-as-failure (absence of positive knowledge) instead of "strong" (presence of negative knowledge, as expressed by the negation of negation in classical (or other) logic). Although many approaches have been proposed to extend Prolog with strong negation, none of those has seen general acceptance so far. Instead, strong negation can be found in a different approach to logic programming:**Answer Set Programming**. The symbols for negation can be`~`

or`¬`

or`naf`

or`\+`

. It depends on the author but generally`¬`

is the strong negation.**Formula**of a logic is the set of words inductively built from "atomic formula" using logical connectives (not, and, or, implies, iff, maybe less, maybe more) and the two quantifiers (adjoined to a variable) "there is" and "for all" (and maybe others). The set of formula `L(F,P)` over signature Sigma = `<F,P>` is said to be a first-order language over the signature Sigma. (See also Wikipedia: Well-Formed Formula). An "open formula" is one with free variables, i.e. variables not bound by quantifiers. What the meaning, if any, of such an open formula is is context-dependent.**Clause**- a general normal form for expressing predicate calculus formulas. It is a disjunction of literals (P1 ∨ P2 ∨ ....) whose arguments are terms. The terms are usually introduced by eliminating existential quantifiers. (from CACM March 1992)**Horn Clause**- a clause containing (at most) one positive literal: H ∨ ~B1 ∨ ... (if Prolog is interpreted in the context of classical logic, the`~`

is the strong negation). The term**Definite Clause**is used to denote a clause with exactly one positive literal. Prolog programs can be viewed as a set of definite clauses in which the positive literal is the head of the rule and the negative literals constitute the body or tail of the rule. (from CACM March 1992). A Horn Clause without negative literals is called a**fact**`H`, otherwise a**rule**. Note that a clause without the positive literal can be interpreted as a**logical constraint**(not to be confused with constraint logic programming). These are not supported by Prolog (but are supported by ASP systems).**Horn Clause (alternative)**(alternative, from a text by David Warren): A Horn clause in a first-order logic is a universally quantified implication in which conjunction of atomic formulas implies an atomic formula. The Horn clause in `∀X∀Y∀Z (`arc(X,Y)`

∧`path(Y,Z)`

⇒`path(X,Z)`

)` could be a part of a description of paths through a graph. (This definition has the advantage that it justifies calling`A :- B,C,D`

a Horn clause in a logic that does not allow the equivalence A⇒B = ¬A∨B, which is intuitionistic (positive) logic, which is the logic that really applies to Prolog even though it is often said that we are dealing in classical logic).**Intuitionistic Logic**An ensemble of logics (and more widely, a philosophical stance) which does not accept the premise of classical logic that every sentences be necessarily labeled exactly one of "true" or "false", but accepts that some statements may remain "not labeled" until a (human) decision has been taken about how to proceed. In effect, what Prolog does is label sentences true if it can -- and otherwise fail, leaving the question open. It thus actually works in a fragment of positive intuitionistic logic rather than classical logic. Which makes complete sense from a programming perspective. Note that in particular, the implication A⇒B is NOT equal to ¬A∨B in Intuitionistic Logic. Instead it is taken to be statement like "Given a proof of A, you are then allowed to state that you also have a proof of B". See also: Uniform Proofs as a Foundation of Logic Programming (Dale Miller et al. 1991) and the Introduction of Logic programming with strong negation and inexact predicates (Gerd Wagner, 1991). More on the philosophy at the Stanford Encyclopedia of Philosophy: Intuitionsitic Logic and Constructive Mathematics. Also, the problem of the Continuum Hypotheses.

**Resolution**(see Robinson 1965: "A Machine Oriented Logic Based on the Resolution Principle", which can be found on the Interwebs for free): A single inference step used to prove the validity of predicate calculus formulas expressed as clauses. In its simplest version: (P∨Q) ∧ (P∨R) ⊢ (Q∨R) which is called the resolvant. (from CACM March 1992). See also: Wikipedia entry**Linear Resolution****SL-Resolution**(sometimes**SL Refutation**) described in Linear resolution with selection function PDF) (Kowalski and Kuehner, 1971) stands for "Linear Resolution with Selection function" (probably backronymed) is an original automated theorem proving proof idea whereby Robinson resolution is applied to a single literal in each step: _Linear resolution with selection function is a restricted form of linear resolution. The main restriction is effected by a selection function which chooses from each clause a single literal to be resolved upon in that clause. This and other restrictions are adapted to linear resolution from Loveland's model elimination._ (adapted from Shanahan)**SLD-Resolution**(sometimes**SLD Refutation**) described in Predicate Logic as Programming Language (Kowalski 1974) it stands for "SL-Resolution for Definite clauses" and is SL-Resolution applied to Horn clauses. SLD-Resolution is still non-deterministic and needs to be further restricted to be implementable.**Prolog**is the result of applying a restricted form of SLD-Resolution to the definite clause subset of predicate calculus, as described by Colmerauer, Kanoui, Roussel, Pasero in "Un Système de Communication Homme-Machine", 1973 (Research Report, Université Aix-Marseille Luminy): The leftmost atom in a goal clause is always chosen to resolve against, definite clauses are tried top-to-bottom order and a depth-first search is employed, for efficiency reasosn, the unification algorithm omits the occurs check. In fact, SLD-resolution is not strictly speaking a form of SL resolution, since it is more liberal in the selection functions it allows. (text adapted from "Solving the Frame Problem" by Murray Shanahan, MIT Press, 1997).

"SLD resolution can be understood procedurally as executing a nondeterministic program with procedure calls" (David Warren),

**SLDNF-Resolution**(sometimes**SLDNF Refutation**): SLD Resolution with "Negation as Failure" to implement a "weak negation" operator.**SLG-Resolution**A proof strategy whereby intermediate results are cached (**tabled**, this is called**tabling**and sometimes**memoing**). This makes it possible to write programs without having to pay special attention to infinite descent during depth-first search if the clauses are badly ordered. Prolog behaves more like a bottom-up theorem prover. (This may have been called "OLD Resolution with Tabulation" OLD Resolution with Tabulation, Taisuke Sato, July 1986 alias "OLDT Resolution" in the 80s, not sure). See: tabling. Certainly a feature that all modern Prolog systems should have and that should be taught.**Refutation completeness**A property of the SLD proof method in that SLD is "refutation complete" for Horn clauses. This means that if a ground answer is a logical consequence of a program then there is an SLD refutation that generates/accepts that answer (or a more general one). There may, however be some proofs paths that are infinite in length. Since Prolog must search this tree for the answers, its depth-first search may get caught on an infinite path, before it gets to the answer.

From the above, we have:

- Resolution (Robinson 1965) (basic principle used in systems like "Markgraf Karl Refutation Procedure" of mid-70s .. mid 80s, with additional control heuristic to direct the search). Also in Hewitt's PLANNER language (not sure whether implemented, there are obviously efforts at retconning precedence & history here; in the end it doesn't matter ... next problem!).
- ⇒ Linear Resolution (?)
- ⇒ SL Resolution (Kowalski & Kuehner 1971). Kowalski is cited as: "I can recall trying to convince Hewitt that Planner was similar to SL-resolution."
- ⇒ SLD Resolution (Kowalski 1974)
- ⇒ PROLOG using (a modification of) SLD-Resolution (Colmerauer et al. 1973)
- ⇒ PROLOG using SLDNF (many other branches exist)
- ⇒ PROLOG using SLDNF and SLG

Completely different approaches at building proof systems exist: Those based on Sequent Calculus, bottom-up provers, Tableaux-based, Answer Set Programming (Stable Models) and probably others.

- Stack Overflow: Fact, Rule, Procedure, Predicate
- Glossary of Logic terms (PDF) by Marc Cohen

- A
**proper list**or a**closed list* is a list that has the**empty list`[]`

as the terminating element of the

Example of a proper list: an empty list `Empty` and a list of length 3 `List1` and of length 2 `List2`.

↙"tip" List1 ------>[|] / \ 1 [|]<-------List2 / \ 2 [|] / \ ↙"fin" 3 []<----- Empty

The list `Empty` could also appear simply like this. There is no way to find out which of the above and the below is "really" the case from Prolog:

Empty ------>[]

- The
**backbone**is formed by a series of**list cells**which are compound terms with name `[|]` and arity 2. In Prologs other than SWI-Prolog, the compound name is traditionally `.` -- but `.` is used for SWI-Prolog dicts now. A backbone can only be traversed from the "tip" to "fin". There is no way to fin a "prior list cell". - A variable
`List1`holding a list can be though of a referencing a "the first list cell" of the backbone. The predicate is_list/1 can be used to verify that the term reachable from`List1`is indeed a proper list. - A variable
`List2`referencing a list cell further along the backbone sees a shorter list. Nevertheless, the data structure is**shared**between`List1`and`List2`and this fact is often exploited for (example, if an element reachable from both`List1`and`List2`is further instantiated, from`X`to`2`

for example, then predicates holding either of`List1`or`List2`will see this change). See also: duplicate_term/2 and copy_term/2. - An
**element**of a list is any term (atomic or compound) that can be found at argument position 1 of a list cell. - The
**empty list**is a distinguished list of length 0. In SWI-Prolog it is represented by a dedicated atomic term which is not an atom (other Prologs may have subtly differing representations) **Head**and**Tail**: A list can be "destructured" into a**Head**and a**Tail**by unifying it with an expression like`[H|T]`

.- The
**Head**is a sequence of n>= 1 elements, most often just 1 element. - The
**Tail**is a variable denoting the rest of the list (of length >=0) after the Head. The Tail can unifiy with`[]`

. - Examples:
`[H|T]=[1,2,3]`

`[H1,H2|T]=[1,2,3]`

`[H1,H2,H3|T]=[1,2,3]`

(`T`will not be`[]`

- the list without the first three positions is the empty list)`[H1,H2,H3,H4|T]=[1,2,3]`

will fail.

- The
**Tip**and**Fin**(this is my terminology, but it's pretty useful, especially when using open list; more precise than "front" and "end").- The
**Tip**of a list is the first list cell of the backbone (if it exists) or the empty list in case of an empty list (a bit synonymous with start of a list, beginning of a list, front of a list) - The
**Fin**of a list is whatever is found on argument position 2 of the last list cell (if it exists). In a proper list, this is always the empty list. - Now we can talk about directions "tipwards" and "finwards"

- The
**Prefix**and**Suffix**- A
**Prefix**of a list is a sublist appearing at the start of a list, encompassing 0 <= n <= length list cells. It may be the empty prefix, which is`[]`

. The empty list has an empty prefix. - A
**Suffix**of a list is a sublist appearing at the end of a list any term (atomic or compound) that can be found at argument position 2 of a list cell (alternatively, or can appear as a Tail in destructuring). The last list cell (alternatively, a list of length 1) has an empty suffix. The empty list has no suffix (it*is*the suffix). - We can consider append/3 to
*define*the meaning of Suffix and Prefix. These all pass:`Prefix=[], Suffix=[], append(Prefix,Suffix,[]).`

`Prefix=[], Suffix=[1,2,3], append(Prefix,Suffix,[1,2,3]).`

`[H|T]=[1,2,3], Prefix=[H],Suffix=T, append(Prefix,Suffix,[1,2,3]).`

`[H1,H2|T]=[1,2,3], Prefix=[H1,H2],Suffix=T, append(Prefix,Suffix,[1,2,3]).`

`[H1,H2,H3|T]=[1,2,3], Prefix=[H1,H2,H3],Suffix=T, append(Prefix,Suffix,[1,2,3]).`

- A
- List operations , obtaining a new list by destructuring an existing list or constructing a new list from other lists:
**prepend/add prefix/head**:`Newlist = [X|OldList]`

. If the list is seen as a stack, this is**push**. This is efficient.**append/add suffix/tail**:`append(OldList,Tail,NewList)`

. This is extremely expensive as it involves copying`OldList`. Practically never done. To borrow Perl terminology, this is`shift`

(although Perl "shifts" at fin).**remove a head/prefix, remove at tip**.`OldList = [X|NewList]`

If the list is seen as a stack, this is**pop**. This is efficient.**remove a tail/suffix, removing at fin**:`append(NewList,Tail,OldList)`

. This is extremely expensive as it involves copying`OldList`into`NewList`. Practically never done. To borrow Perl terminology, this is`unshift`

(although Perl "unshifts" at tip).

**Special case: The open list***

An open list can still grow its backbone (it can be "further instantiated") because its Fin is not set: it is "empty cell". If the there is a variable naming the Fin, say `Fin`, then `Fin` is an unbound variable, `var(Fin)`

returns true.

An open list is transformed into a closed list by unifying that `Fin` with `[]`

.

A special case is the "empty open list", which is really just any unbound variable. (The future history of an unbound variable is always open, it could become anything, even the tip of a proper list).

Example of a nonempty open list:

↙"tip" List1 ------>[|] / \ 1 [|] / \ 2 [|] / \ ↙"fin" 3 <empty> <---------- Fin

An open list is simply created by: `OpenList = [1,2,3|Fin].`

. After `Fin=[]`

it is then a proper list.

A *difference list" (which is actually confusing terminology) is really just a "list difference": two variables which refer to two positions in a list: `X=[a,b,c,d], X=[a,b|Y].`

From there, you can infer the "list difference", which is the `X` list minus the `Y` list: `[a,b,c]`

(and which in extremis can be generated with `append(LDiff,Y,X).`

)

<--> LDiff = [a,b] X Y | | [a,b,c,d]

These two references can be packed into a term to pass them to other predicates: `p(X-Y). p(X/Y).`

But they should not (why waste cycles?). Just use `p(X,Y).`

The above construction is useful when the underlying list is an "open list", where `Y` points to the empty cell "fin" (the write position) where new elements are appended by a producer, and `X` is trailing behind (the read position) where elements are consumed by a consumer. The "list difference" then is the current buffer, which is empty if `X==Y, var(X), var(Y)`

and EOF is expressed by `Y=[]`

.

Here is another representation of the above:

X ------->[|] ^ / \ | "list difference" X-Y is a [|] | [a,b] / \ V b [|]<------------- Y / \ c [|] / \ d [] <--- list properly ends in []: proper list

When based on an open list, when the empty cell at the "backbone fin" is called `Fin` and takes the role of `Y` above and the 'X' is called 'Tip':

`Tip=[a,b,c,d|Fin]`

Tip ----->[|] + / \ | "list difference" Tip-Fin is a [|] | [a,b,c] / \ + b [|] / \ c ~empty cell~ <--- Fin

We can obtain an element `V` at the tip: `Tip=[V|NewTip]`

and use `NewTip` as new `Tip` in the next activation:

NewTip ----> [|] + / \ | "list difference" NewTip-Fin is b [|] | [b,c] / \ + c ~empty cell~ <--- Fin

Analogous to imperative programming with pointers, `Fin=[d|NewFin]`

grows the open list with `d`

, and yields a fresh variable `NewFin` denoting the new fin, which is an empty cell.

Tip ----->[|] + / \ | "list difference" Tip-NewFin is b [|] | [b,c,d,] / \ + c [|] / \ d ~empty cell~ <--- NewFin

This can continue for some time. Mayn algorithms do not consume at the tip but just append at the fin. In any case, when we are done: `Fin=[]`

, which closes the list. Once that unification has been performed, a proper list can be found at `Tip`:

Tip ----->[|] + / \ | "list difference" Tip-Fin is x [|] | [x,y,z] / \ | y [|] | / \ + z [] <--- Fin after Fin=[] - there is now a proper list at Tip

or if `Tip` and `Fin` were equal when the unification is performed, in which case the "list difference" is the empty list:

Tip------> [] <----- Fin after Fin=[] - there is now a proper list at Tip

The "empty open difference list" is evidently trivially an empty cell (or two unbound variables denoting the same empty cell): `Tip=Fin`

. It's a bit borderline. Is this really a "list"?

Tip------> ~empty cell~ <----- NewFin

It can **fail** or **succeed** of course (or throw an exception, rudely moving us back from logic-land back into programming-land), but if it succeeds:

- It can
**accept**the argument tuple passed:`length([a,b,c],3)`

, When interpreted as function`length(List) -> Length`

,`length(L)`

is evidently surjective (in its domain), so one could say:`length([a,b,c],3)`

**verifies/checks**the length of list`[a,b,c]`

`length([a,b,c],3)`

**verifies/checks**whether list`[a,b,c]`

is a member of the preimage of 3 (technically of the set {3}).

- Going in the direction of (potential) information loss implied by a function, from "list" to "length", if
`L`is unbound at first:- This is often called "going forward"
`length([a,b,c],L)`

**computes/deduces**`L`from`[a,b,c]`

or**maps**`[a,b,c]`

to`L`- This information loss idea should be made more precise (there must be a paper somewhere on this!). Note that some predicates can be "fixed" so that they do not lose information "going forward". This is "reversible computing" in Prolog:
`append([a,b],[c,d],X)`

.`X`contains no information about the "input"`append_reversible([a,b],[c,d],[X,PrefixLen])`

.`[X,PrefixLen]`

contains enough information to "get back" to the input!

- Going in the direction of information gain implied by a reverse function, Prolog can:
**Hallucinate**information (this is a bad idea):`length(L,3)`

yielding`[a,b,c]`

? NOPE!**Propose**a most generic template containing unbound values that unifies with any member of the preimage:`length(L,3)`

yielding`[_,_,_]`

. Yes!**Generate**the members of the pre-image if they can be enumerated:`member(X,[a,b,c])`

yields`a`

,`b`

,`c`

in turn.- If the pre-image is higher-dimensional, this can become complex:
`append(L1,L2,[a,b,c]).`

yields`L1 = [],L2 = [a, b, c] ; L1 = [a],L2 = [b, c] ; L1 = [a, b],L2 = [c] ; L1 = [a, b, c],L2 = []`