Glossary

Although originally seen as a highly ambitious concept of computer programs that cannot be distinguished from human beings (as in the Turing test), AI is now used to describe computer programs that 'Learn and adapt' using the environment around them. The previous view of AI is now referred to as Strong AI.

Assembler is a low-level language used to program micro-processors directly. It is essentially a human readable form of machine code, and can therefore be very efficient, but very difficult, to program with.

Automated Theorem Proving (ATP) is the autonomous proving of mathematical theorems by a computer program. Logic programming was developed as a side-effect of research into ATP, with lots of work being done in inference rules to simplify logical sentences. 'E' and 'Otter' are examples of high-performance theorem provers, 'E' using purely equational calculus, whilst the latter makes use of the resolution principle in first order logic.

Backtracking is a feature of many languages developed when computers had highly limited memory size, and were therefore unable to store previous computations or a large amount of state information about a running program. Backtracking means that the interpreter exhausts a possibility in the search tree, then backtracks to the last choice point, where it carries out it's work along any unvisited paths so far. Algorithms featuring backtracking for traversing trees include Depth First Search and Breadth First Search.

Backward chaining starts with a list of goals and works backwards to see if there are data available that will support any of these goals. An inference engine using backward chaining would search the inference rules until it finds one which has a Then clause that matches a desired goal. If the If clause of that inference rule is not known to be true, then it is added to the list of goals.

Boolean connectives are used to join atoms together to form a formula. The primary connectives are NOT (¬), AND (∧), OR (∨), IMPLIES (→), IF-AND-ONLY-IF (↔), T (truth) and ⊥ (falsity).

Clausal form is one of the normal forms in which a formula can be represented. A formula in clausal form can take up a lot more space than in a simplified form, but will ultimately contain no quantifiers and therefore be operable on by the resolution rule.

A compiler is used in many languages to translate the source code written by the programmer into machine code, executable by the computer. There are often intermediate stages of compilation (e.g. Assembler and Java-bytecode) but most logic-programming languages are interpreted rather than compiled.

Concurrent programming involves one or more threads running simultaneously. The advantage of concurrent programming is in multi-processor environments, when increases in speed can be substantial.

Constraint Programming is where relationships between data are described in terms of constraints. Instead of specifying steps to follow (ie an algorithm), only properties of solutions are specified.

The control structure is the data structure used by a programming language to store the current state of the computation and how it is traversed.

These laws provide a simple way to push negations inside closed expressions and are required when reducing a formula to Negation Normal Form.

Declarative Programming has two different meanings.
1) Programs that describe what something is, not how it is created. For example, webpage code describes what the page should look like but not how to display it.
2) Programs that are written in a functional, logical or constraint programming language.

Depth-first search (DFS) is an algorithm for traversing or searching a tree, tree structure, or graph. The algoritm extends the current path as far as possible before backtracking to the last choice point and trying the next alternative path.

First Order Logic is a powerful extension of Propositional Logic. This logic introduces quantifiers. The two quantifiers are the Existential Quantifier (∃) and the Universal Quantifier (∀). ∃x, ƒ(x) says that there exists an x, such that ƒ(x) is true. That is ƒ is satisfiable. On the other hand, ∀x, ƒ(x) says that under no circumstances is ƒ false. That is ƒ is valid.

A formula is essentially the 'if test' in propositional calculus. Formulas are made up of atoms joined together by boolean connectives. Formulas can be represented as formation trees, in which the nodes are atoms or connectives. Brackets are used to disambiguate the meaning of formulas, and binding conventions apply to the relevant connectives. Formulas take on a boolean value.

Letters of the alphabet are formulas.
If ƒ is a formula, ¬ƒ is also a formula.
If ƒ1 and ƒ2 are formulas, then ƒ1~ƒ2 is a formula, where ~ is a boolean connective.
Nothing else is a formula.

Forward chaining starts with the available data and uses inference rules to extract more data until an optimal goal is reached. An inference engine using forward chaining searches the inference rules until it finds one where the If clause is known to be true. When found it can conclude, or infer, the Then clause, resulting in the addition of new information to its dataset.

The functional programming paradigm treats computation as the evaluation of mathematical functions. No state information is held during execution unlike Procedural programming which relies on the execution of sequential instructions.

Fuzzy Sets form part of Fuzzy Logic, and deal with the 'member of' relation in set theory. Unlike classical set theory, Fuzzy Sets allow different degrees of membership using a scale ranging from 0-1, that is non-member to full-member.

A conclusion in a logic programming query, which if made true allows the language interpreter to return success for the query. Goals are the same as sub-goals, which are the "then" clauses of an "if... then..." query. If all the sub-goals of a query can be proven true, then so can the antecedent.

Higher-Order functions are often added to programming languages to reduce coding for programmers, and help prevent repetitious blocks of code occurring. They take one or more functions as input, and output another function. In logic programming these are referred to as Meta-Programs since they deal with programs rather than functions.

A Horn-clause is a clause with at most one positive literal. If a Horn-clause has exactly one positive literal then it is known as a definite clause. Similarly, a Horn-clause with no positive literals is referred to as goal.

The imperative programming paradigm takes on the 'Do this, do that' approach, forming a sequential statement list in the code. Unlike logic-programming, imperative languages state 'how' the computation is to take place, rather than 'what' is to be computed.

An implementation constraint puts limits on coding or construction; for example, required standards, platform, or implementation language.

Indeterminacy means that in a sequence of events, it is down to chance which event will occur next. This occurs in concurrency of mathematical logic based logic-programming where the concurrency is implemented using message passing systems. These messages arrive in random order and therefore indeterminacy results in the order of execution.

An inference engine is a computer program that controls how "if... then..." rules are applied to the knowledge base (facts and relationships) of a database in order to conclude (infer) new facts or relationships.

Inference rules are logical rules which allow new logical formulas to be derived from existing ones, usually in pursuit of a conclusion. There are many rules, which can be replaced by the rule of resolution providing the formulas are in clausal form.

An interpreter is a program which itself runs other programs. Unlike a compiler, the interpreter will 'interpret' the source code directly without first translating the source code into machine code.

Logical Consequence is the relation that holds between a set of sentences and a conclusion that can be drawn from them. If the set of sentences A...An can be used to show R, then we say A...An |- R.

Logical languages deal with extraction of knowledge from basic facts. Logic programming makes use of pattern-directed invocation of procedures from assertions and goals. They answer queries via searching. Searching is done via forward-chaining and backward-chaining.

A sentence is a formula with no free ( i.e. Unbound ) variables. Since all the variables in a sentence must be bound, sentences always have a boolean value in a given structure.

Modal logic is an extension to standard logic that allows modalities to be expressed in three ways. A sentence is either 'possible', 'necessary' or 'contingent'. These classifications have much in common with propositional validity but are not used as a basis for logic programming.

Natural Language Processing (NLP) is the study of computer understanding and generation of natural human languages.

Negation Normal Form is a normalisation for formulas where negation occurs only immediately above propositions. This can be brought about using equivalences and the De Morgan laws. Negation Normal Form is a step towards Clausal Form of Disjunctive Normal Form.

Nondeterminism is referring to a computational property that may have more than one result.

OOP is a relatively new paradigm which emphasises modular programming and data separation. The primary concept of OOP is breaking a large problem down into smaller problems, which are solved and then called by other methods within the program.

Perfect play is an idea of game theory, in which the behaviour of a player is that which leads to the best possible outcome for that player.

The procedural programming paradigm is where code is separated up into functions or methods that can be called individually. This prevents code duplication in moderately complex programs and makes layout easier, allowing for modular coding. Procedural programming is also used as a synonym for imperative programming.

A propositional atom is simply a variable, as in maths, which can take on either true or false as it's value. Atoms cannot be separated into 'sub-atoms'; they are atomic.

Propositional calculus ( logic ) is a subset of First Order Logic. It can be referred to as 'The study of if-tests'. That is, we can express atomic statements in terms of if (something is true) then (do something else). Boolean connectives are used to expand on this, creating a final statement (formula) with a true or false value. The three 'ingredients' in propositional calculus are atoms, boolean connectives and punctuation. Propositional calculus is a deduction system on objects (propositions) which can be used to prove propositional relations.

The act of removing parts of a search tree in order that they won't be computed.

Resolution is an inference rule that can be used in place of the other inference rules providing the formulas in question are in clausal form. Resolution takes two clauses, (a clause being a disjunction of literals) and produces a new one from them by eliminating atoms whose complement appears in one of the original formulas.

The Scientific Community Metaphor is used as a metaphor to employ systems displaying certain traits mirrored in the Scientific Community.

A search tree is a data-structure used by many logic-programming interpreters to find solutions to a query. Since all data structures can be represented as a tree, this is a logical and efficient way to retrieve data.

Semantics essentially means 'meaning'. The semantics of a logic describe the meaning of it.

Skolem Normal Form applies to First Order Logic in which all existential quantifiers (∃) are removed and replaced in some way by universal quantifiers (∀). To Skolemize a formula, the following second-order equivalence is used as the main principle of converting to Skolem Normal Form:

Stable Model Semantics is a tool used to add negation to many logic-programming languages. Rather than mirror the mathematical view of negation, it assumes that all atoms not held as true by a program are therefore false. Stable Model Semantics also goes on to define a family of models of a logic program.

Terms are constants or variables used to name objects. A special term, known as a Ground Term, is one that does not involve a variable.

The Turing test is a simple test to determine the effectiveness of the conversational ability of a machine with humans. If a human cannot tell the difference between a conversation with a machine and with another human, then the machine will pass the test.

A type system in a programming language is a way of classifying different data structures or elements. This classification can then be used as a code check in order to ensure that various data types match where appropriate.

A variable in a logic programming language which is initially undefined but which may get bound to a value or another logic variable during unification of the containing clausewith the current goal.

The validity of a formula gives some insight into when the formula is true. A valid formula is always true, A∨¬A for example. A satisfiable formula is true in some, but not all, situations.