This is an introductory page to:
Programs using XSB
- XSB is an open-source Prolog
Programs using Flora
- Flora is an open-source logic
programming system written in XSB Prolog
Technology Theorem Proving (PTTP)
- PTTP is a theorem
prover for first-order logic written in Prolog
According to Wikipedia on Logic Programming
programming is a type of programming paradigm which is largely based on
program written in a logic programming language is a set of sentences in
logical form, expressing facts and rules about some problem domain.
is a general-purpose logic programming language associated with artificial
intelligence and computational linguistics.
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.
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.
axiom is a statement interpreted as a general truth.
Some axioms correspond to what are generally known as “rules”.
of a logical implication may correspond to the “if” part of a rule
of a logical implication may correspond to the “then” part of a rule
Some axioms correspond to what are generally known as “facts”.
Axioms of propositional logic consist of atoms
which may be connected or negated ('¬')
atom comprises a function or predicate term having zero or more argument
are connected by conjunction (e.g., '∧') or disjunction (e.g., ‘∨’)
may also be connected by implication (e.g., '→')
and negated atoms are collectively known as literals.
A literal represents the truth or falsehood of an atomic proposition.
contradiction occurs when a proposition is true and false
logic is inconsistent
if it can prove a contradiction
The explicit representation of falsehoods is required by the open-world
semantics defines a means of handling contradiction using a third
Prolog supports the well-founded semantics (as does Flora)
In effect, the well-founded semantics allows mixing of the open- and closed-world
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.
quantified (∀) as in “for all”
quantified (‘∃’) as in “there exists”
Higher-order logics may allow for variables to range over
functions or predicates.
provides a higher-order syntax known as Hilog.
Defeasible logics allow for exceptions to axioms.
Prolog is simply a restricted form of logic in which axioms in which:
are universally quantified
consequent is an atom
antecedent is a possibly empty conjunction of literals
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
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 &
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
implements “selective, linear, definite clause” (SLD) resolution.
Prolog adds “tabling” in SLG resolution (c.f., Datalog).
uses proprietary, heuristic proof procedures
One of our favorite works is Mark Stickel’s and
Jerry Hobb’s “Interpretation
In the course of that work, Stickel developed a
Prolog technology theorem prover (PTTP).
TTP differs from Prolog in its use of
with the occurs check for soundness,
iterative deepening search instead of unbounded depth-first search to make
the search strategy complete, and
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.
 the difference between
functions and predicates is a detail discussed here
 Note that implication
adds no expressive power since A→B is logically equivalent to ¬A∨B.
Copyright © 2018 by Automata, Inc. All rights reserved.