Prolog

Prolog is a programming language, but it differ from procedural or object oriented languages. It is used mostly by logic-oriented programs. So let define some basics.
Atom is any string which begins with lower case and consist letters,numbers and underscore character, or any string enclosed in single quotes, or special character. For example

• a,b,c, ab, aB, aC_ are atoms.
• 'asb',''&^%&#@$ &*' are atoms.
• special characters are @= and ====> and ; and :- and etc...

Number - any number.
Variable is a string of letters,numbers and underscore, which begins with uppercase letter or with underscore. Examples

• X, Y, AX, Axx, _aAb, _ABA are variables
• _ is special variable and it is called the anonymous variable.

Complex term (or compound term) is an atom(called functor) plus arguments, which are terms or variables or numbers or atoms.

The prolog program is consist of several rules or facts, which are separated by '.'.

The rule is of the form

head :- body.

and is read as "If body is true then head is also true". When the body is empty then it called fact and is written without :- operator. The head is complex term, but the body can have several terms which used together with conjunction(',') or disjunction(';'). For example
a(x) :- b(x), c(x).
If b(X) and c(X) are true then a(X) is true.
f(x) :- d(x); e(x).
If d(X) or e(X) are true then f(X) is true.

So we write some rules, but what the prolog program do. It just reads the rules and wait, until we ask some questions. Before discussing some real examples,let I give this link to the site of SWI-prolog(the popular implementation). There you can download and install the installation packages for variety of OS. After finishing, you can lunch the environment itself or write the prolog code in file with extension pl and lunch it. In second case SWI will read the rules from that file and get ready to answer the questions, in first case you must manually add rules.

Now let's discuss a simple example. Let a,b,c,d be the some properties of X and

a(X) :- b(X) , c(X).
d(X) :- b(X) ; c(X).

and 1 has properties b and c, 2 has property c.

b(1).
c(1).
c(2).

So now we can write down this into a file and run it, after it let give it some questions.
?- b(1)
true
it answers true, because 1 has the property b.

?- a(1)
true
it answers true, because 1 has the property b and c and from rule 1 has property a.

?-a(2)
false
because 2 has property c but hasn't property b so it hasn't property a.

In same way
?-d(1)
true

?-d(2)
true

Now an unusual question.
?-d(3)
false
because we don't know anything about 3.

This language can be showed simple in first view, but using it we can write some hard programs, which takes several time less time and less code size than in other programming languages. Next time I will tell more about Prolog and about ncDP prover program. Also I want to mention this site where you can find a good free book about Prolog.

Soundness and Completeness

In first post I define provability of propositional formula. But propositional formula can be interpreted as a Boolean function and if it is equal to true for every arguments then we say that propositional formula is tautology. In similar way if proposition is equal to false for every arguments then it called contradiction.
Let's discuss L propositional calculus, where
Connectives are and →.
Axioms are

1. A→(B→A).
2. (A→(B→C))→((A→B)→(A→C)).
3. (B→A)→((B→A)→B)
   

And the only inference rule is MP(Modus Ponens).

This system has good properties, such that every tautology is provable L and any provable formula is tautology.The first one is called Completeness and anothe one is called Soundness

Theorem(Soundness) ├P => P is tautology.

Theorem(Completeness) P is tautology => ├P.

EBNF and Boost.Spirit

EBNF(Extended Backus-Naur Form) is a syntax notation used to write grammars. It distributed so that it was standardized by ISO. The Spirit is a parser library for EBNF writed in C++. It is distributed with Boost. So let introduce them with examples. In previous post we discuss normal forms,now let write the grammar of CNF using EBNF. At first we need to define proposition.

proposition ::= alpha_p alnum_p*;

alpha_p is alphabetic character, alnum_p is alphabetic or numeric character,* means zero or more repetition of alnum_p. For example "ab78" is a proposition but "7ab8" is not, because the first symbol must be a letter. The next one is a literal.

literal ::= proposition | proposition;

Literal is a proposition or negation of proposition. We also need to define intermediate formula, which is a disjunction of literals, let call it term.

term ::= ( literal (⋁ literal)* );

CNF_formula ::= term (⋀ term)*;

The brackets are added to prevent ambiguity(for example A⋁B⋀C can be interpreted as A⋁(B⋀C) or A⋁(B⋀C) ). Usually lines write at inverse sequence. At first define the main formula , and then define other rules. So the grammar of CNF in EBNF is:

CNF_formula ::= term (⋀ term)*;
term ::= ( literal (⋁ literal)* );
literal ::= proposition | proposition;
proposition ::= alpha_p alnum_p*;

alpha_p and alnum_p are not defined in EBNF, I can define them, but it is not necessary because we will use this grammar in Spirit, in which those are predefined. In Spirit used modified version of EBNF, because of the limit of C++ grammar. Instead of space used in EBNF as a separator of lists, in Spirit they use >> operator. In place of ::= use =, and * operator is changed from postfix to prefix. Every line of EBNF can be stored in variables of type rule.
This is the analog of CNF grammar in Spirit. We use other symbols for connectives to write code using only ANSI symbols. &=⋀ ;|=⋁; ~=;

CNF_formula = term >> *( '&' >> term);
term = '(' >> literal >> *( '|' >> literal) >> ')';
literal = proposition | '~' >> proposition;
proposition = alpha_p >> *(alnum_p);

Now we can parse any string using CNF_formula rule.

parse(str, CNF_formula,space_p);

where the third parameter is the skip rule. We can combine those rules into one grammar class

#include <boost/spirit/include/classic_core.hpp>
using namespace BOOST_SPIRIT_CLASSIC_NS;

struct CNFGrammar : public grammar<CNFGrammar>
{
template <typename ScannerT>
struct definition
{
definition(CNFGrammar const& /*self*/)
{
CNF_formula = term >> *( '&' >> term);
term = '(' >> literal >> *( '|' >> literal) >> ')' ;
literal = proposition | '~' >> proposition;
proposition = alpha_p >> *(alnum_p);
}

rule<ScannerT> CNF_formula,term,literal,proposition;

rule<ScannerT> const&
start() const { return CNF_formula; }
};
};

And use it to write simple program which parse the input string.

int main()
{
string str;CNFGrammar g;
while (getline(cin, str))
{
if (str.empty() || str[0] == 'q' || str[0] == 'Q')
break;

if (parse(str.c_str(),g,space_p).full)
cout << "Parsing succeeded\n"; else cout << "Parsing failed\n"; } return 0; }

CNF,DNF and NNF

As we know the set { ,⋀,⋁, →} of connectives is functionally complete. We can eliminate → connective and the result set remain functionally complete, because → Boolean function can be written in form of p⋁q (p→q), it easy to see when we write down the truth tables. But the remain system has more properties than just the completeness, we can write any propositional formula in some normal forms, which we define now.

NNF(Negation Normal Form)
A formula is in NNF when it consists only ,⋀,⋁ connectives and connective used only on propositions(sometimes called atomic formulas). For example ((p⋀q)⋁(r⋀t)) formula is in NNF, but ((p⋀q)⋁(r⋀t)) formula is not in NNF. We can also define an algorithm which transfer a propositional formula into NNF.
Algorithm

1. Write formula using only ,⋀,⋁ connectives.
2. Push negations in until they apply only to propositions or negation of propositions(called literals), repeatedly replacing by equivalences

p=p
(A⋀B)=A⋁B
(A⋁B)=A⋀B

We can simplify the NNF formula again.
CNF(Conjunctive Normal Form)
A formula is in CNF when it is in form of A1⋀A2⋀A3⋀...An where each Ai is in form B1⋁B2⋁B3⋁...⋁Bn where each Bi is proposition or negation of proposition.
It easy to understand that CNF formula is in NNF . And for transforming propositional formula into CNF we can at first transform it into NNF then

• Push disjunctions in until they apply only to literals, repeatedly replacing by equivalences

A ⋁ (B ⋀ C)= (A ⋁ B) ⋀ (A ⋁ C)
(B ⋀ C) ⋁ A= (B ⋁ A) ⋀ (C ⋁ A)

DNF(Disjunctive Normal Form)
A formula is in DNF when it is in form of A1⋁A2⋁A3⋁...An where each Ai is in form B1⋀B2⋀B3⋀...⋁Bn where each Bi is literal. If formula is in DNF then it is in the NNF also.The same transformation method work for DNF when we swap ⋁,⋀ connectives.

Later we see that CNF is useful when proofing theorems and DNF for refuting.

Boolean functions

Let B={0,1}, then a f:B^k -> B function is called Boolean function, where B^k = BxBx...xB is Cartesian product. The k called the arity of function f, or in other words the number of arguments. It is simple to show that there are 2^(2^k) distinct Boolean functions of arity k. In previous post I mention some functions, so let define them precisely now.
The logical negation function ¬ has arity 1 and truth table is:

p	¬p
0	1
1	0

This function also written as ~ ,NOT and etc...

The logical conjunction ⋀ has arity 2 and truth table is:

p	q	p⋀q
0	0	0
0	1	0
1	0	0
1	1	1

Also written as &,*,AND and etc..

The logical conjunction ⋁ has arity 2 and truth table is:

p	q	p⋁q
0	0	0
0	1	1
1	0	1
1	1	1

Also written as +,OR and etc..

The logical implication → has arity 2 and truth table is:

p	q	p→q
0	0	1
0	1	1
1	0	0
1	1	1

There are 16 distinct Boolean functions of arity 2 and most of them have their own name, but they can be expressed with ,⋀,⋁ and →.In general the set of Boolean functions A called functionally complete if every Boolean function can be defined using functions of set A.
The set { ,⋀,⋁, →} of connectives is functionally complete, so every Boolean function can be written as a propositional formula. There are also other functionally complete sets, and such that sets which consists only one element. For example Sheffer's function (NAND,(p⋀q)) or NOR ((p⋁q)) are functionally complete. In general case the Post's theorem show which sets can be functionally complete.

Propositional calculus

I met many different definitions of propositional calculus, which are mostly incomplete, but of course not conflicting with each other. In Wikipedia article there is a general definition, which covers all other definitions. So let's define it.

Definition

Propositions
A proposition is a statement, which can be true or false. For example "3 is prime" and "4 is odd" are propositions and the first one is true and the second is false. In general we write those propositions with letters and do not care about theirs truths. So let A be the finite set of propositions.
Connectives
Connectives are Boolean operators. In general connectives can have any arity, but often discussed operators with arity 0,1 and 2. Some of connectives are "", "⋀" ,"⋁" and etc. And let Ω be the finite set of connectives.

With propositions and connectives we can define the syntax. The formulas of Propositional calculus construct with the following rules:

1. Any element of A is a formula.
2. If p1,p2,...,pn are formulas and ω is operator of arity n from Ω then ω(p1,p2,...,pn) is a formula also.
3. Nothing else is a formula.

In particular case when discussed only operators with arity less or equal 2, the 2nd step formulated differently.For example when Ω={,⋀,⋁,→,↔} then the formulation is

• If p and q are formulas then p, (p⋀q),(p⋁q),(p→q) and (p↔q) are formulas also.

The next two steps will define the semantic of propositional logic.
Axioms

Axioms syntactically are formulas, but in place of propositions we can put any formula. Let I be the set of formulas.
Inference rules
In general inference rule is a set of formulas,the last one of which called conclusion and others are premises. Like the case of axioms, in place of the propositions in formulas of inference rules we can put any formula. Let Z be the set of formulas.
For example on of the familiar inference rules is the Modus Ponens.

premises - p→q and p
conclusion - q

L=L(A,Ω,Z,I) system we call propositional calculus. Let P be the formula of L. We say that P is provable in L and write ├P if there exist a sequence of formulas such that

• The last formula of the sequence is P.
• Each next formula is a axiom instance or the conclusion of inference rules which premises are the formulas from previous elements of sequence.