This is an introductory page to:

- Logic
Programming
- Logic
Programs using XSB
- XSB is an open-source Prolog
- Logic
Programs using Flora
- Flora is an open-source logic
programming system written in XSB Prolog
- Prolog
Technology Theorem Proving (PTTP)
- PTTP is a theorem
prover for first-order logic written in Prolog

According to Wikipedia on Logic Programming and Prolog:

- Logic
programming is a type of programming paradigm which is largely based on
formal logic.
- Any
program written in a logic programming language is a set of sentences in
logical form, expressing facts and rules about some problem domain.
- Prolog
is a general-purpose logic programming language associated with artificial
intelligence and computational linguistics.
- Prolog
has its roots in first-order logic, a formal logic, and unlike many other
programming languages, Prolog is intended primarily as a declarative
programming language: the program logic is expressed in terms of
relations, represented as facts and rules.
- Prolog
was one of the first logic programming languages, and remains the most
popular among such languages today, with several free and commercial
implementations available. The language has been used for theorem proving,
expert systems, term rewriting, type inference, and automated planning, as
well as its original intended field of use, natural language processing.

A logic program is written as a set of logical sentences known as *axioms*.

- Each
axiom is a statement interpreted as a general truth.

Some axioms correspond to what are generally known as “rules”.

- the
of a logical implication may correspond to the “if” part of a rule__antecedent__ - the
of a logical implication may correspond to the “then” part of a rule__consequent__

Some axioms correspond to what are generally known as “facts”.

Axioms of * propositional *logic consist of

- an
atom comprises a function or predicate term having zero or more argument
terms[1]
- atoms
are connected by conjunction (e.g., '∧') or disjunction (e.g., ‘∨’)
- atoms
may also be connected by implication (e.g., '→')[2]
- atoms
and negated atoms are collectively known as
.__literals__

A literal represents the truth or falsehood of an atomic proposition.

- a
contradiction occurs when a proposition is true and false
- a
logic is
if it can prove a contradiction__inconsistent__

The explicit representation of falsehoods is required by the open-world assumption.

The well-founded semantics defines a means of handling contradiction using a third truth-value.

- XSB
Prolog supports the well-founded semantics (as does Flora)

In effect, the well-founded semantics allows mixing of the open- and closed-world assumptions.

* Predicate calculus* allows for a term to be a variable.

* First-order logic *is a predicate
calculus that allows quantified variables as the arguments of atoms.

- universally
quantified (∀) as in “for all”
- existentially
quantified (‘∃’) as in “there exists”

* Higher-order* logics may allow for variables to range over
functions or predicates.

- Flora
provides a higher-order syntax known as Hilog.

* Defeasible* logics allow for exceptions to axioms.

- Flora
supports a simple, effective form of defeasibility.

Prolog is simply a restricted form of logic in which axioms in which:

- variables
are universally quantified
- the
consequent is an atom
- the
antecedent is a possibly empty conjunction of literals
- negation
is interpreted under the closed-world assumption

In practice, Prolog provides extensions such as aggregation.

XSB Prolog supports both open- and closed-world interpretations of negation.

Flora-2 extends XSB Prolog by allowing first-order logic expressiveness in antecedents.

Theorem proving, in general, is a sophisticated area. In its pure form it has limited commercial application, as discussed at Wikipedia. The primary applications are rigorous proofs in mathematics and in circuit verification, but there are important commercial and regulatory applications in compliance, especially with regard to safety (e.g., in aerospace & aviation).

Nonetheless, theorem proving techniques are important and powerful in many areas of artificial intelligence. When we say techniques, we mean inference using theorem proving techniques such as unification and resolution.

- Prolog
implements “selective, linear, definite clause” (SLD) resolution.
- XSB
Prolog adds “tabling” in SLG resolution (c.f., Datalog).
- Cyc
uses proprietary, heuristic proof procedures

One of our favorite works is Mark Stickel’s and Jerry Hobb’s “Interpretation as Abduction”.

In the course of that work, Stickel developed a Prolog technology theorem prover (PTTP).

TTP differs from Prolog in its use of

- unification
with the occurs check for soundness,
- depth-first
iterative deepening search instead of unbounded depth-first search to make
the search strategy complete, and
- the
model elimination inference rule that is added to Prolog inferences to
make the inference system complete.

The PTTP approach is even better today using XSB Prolog. It is not a theorem prover for proofs many dozens or hundreds of steps long but performs well for answering questions or making decisions that require fewer inferences, which includes most questions and decisions, in practice.

[1] the difference between
functions and predicates is a detail discussed here

[2] Note that implication adds no expressive power since A→B is logically equivalent to ¬A∨B.

Copyright © 2018 by Automata, Inc. All rights reserved.