Re: Hilbert-Style proof in propositional calculus

On Jun 15, 5:54 am, "Robert" <robert.goldw...@xxxxxxxxxxxx> wrote:
Thanks,

frankly I don't care about efficiency (or at least from the very beginnig) -
and yes, constructive proof is what I'm looking for. There are three
standard axioms, such as A1: A -> (B -> C), etc., and modus ponens - and I
want to generate the proof from tautological formulae, e.g. for formule like
A->A, I want to generate that 5 step proof for this formule (instance of
axiom 1, instance of axiom 2, MP, ..., A->A) - and then I want to define my
own axioms and see what happens. And as of now, I'm reading introductory
texts on Prolog, so any 5-line help would do.

[snip]

The topic lends itself to Prolog. Here are some thoughts
about the representation of formulas as Prolog terms and
of proofs as lists of the same.

Where conventionally we write propositional formulas with
infix binary operators (->, OR, &) and unary negation ~,
Prolog terms are mostly simply expressed with "functors"
that are prefix operators. To keep things to a minimum,
let's consider implication and negation as the only
logical operators to use. We could then represent the
propositional variables as Prolog atoms and:

P -> Q represented by imply(p,q)

~P represented by isnot(p)

Although it would be more natural to use not( ) for
logical negation, the keyword 'not' is likely to be
reserved in most Prolog's as a metapredicate. So a
slight compromise is proposed to use isnot( ) as the
alternative.

We can then implement a Prolog predicate which succeeds
for well-formed formulas:

wff(X) :- atom(X).
wff(imply(X,Y)) :- wff(X), wff(Y).
wff(isnot(X)) :- wff(X).

Now let's briefly discuss representing proofs as lists
of (well-formed) formulas, such that any entries (steps)
are either axioms or the result of modus ponens on two
prior entries.

Certainly we need a Prolog predicate that defines the
axioms. For the usual three axioms, this will do:

axiom(imply(X,imply(Y,X))).
axiom(imply(imply(X,imply(Y,Z)),imply(imply(X,Y),imply(X,Z)))).
axiom(imply(imply(isnot(X),isnot(Y)),imply(Y,X))).

It will simplify our coding for a proof if we list
the steps in reverse order, a second compromise to
what would perhaps be most natural. That allows
us to write:

proof([ ]). /* empty list is a proof by convention */
proof([H|T]) :- axiom(H),!,proof(T).
proof([H|T]) :-
member(A,T),
member(imply(A,H),T), /* H obtained by modus ponens */
!,
proof(T).

I've thrown a couple of cuts ! into the clauses for
proof, not because we obtain a greatly efficient
implementation this way, but because it reflects the
deterministic nature of the predicate. I.e., it
doesn't matter if a step can be justified in more
than one way, a valid step is a valid step.

The above basically says a list of formulas is a
proof if the last step (Head of the list) is valid
and everything before (Tail of the list) is also
a proof.

This is a start, but more interesting predicates
remain to implement: define tautology, and if a
formula is a tautology, construct a proof.

regards, chip
.

Relevant Pages

  • Re: Complex Subset Computing in Prolog
    ...    variables is unknown build something like distinct. ... There is often confusion when lists and sets are used (in Prolog or ... but let's do this for Prolog) and this pops up ... list representation that is not unique. ...
    (comp.lang.prolog)
  • Re: Complex Subset Computing in Prolog
    ... There is often confusion when lists and sets are used (in Prolog or ... but let's do this for Prolog) and this pops up ... almost always when the subset predicate raises its head. ... list representation that is not unique. ...
    (comp.lang.prolog)
  • Re: Complex Subset Computing in Prolog
    ...    variables is unknown build something like distinct. ... There is often confusion when lists and sets are used (in Prolog or ... but let's do this for Prolog) and this pops up ... list representation that is not unique. ...
    (comp.lang.prolog)
  • Re: An instance of Russells paradox?
    ... >>> of lists is actually syntactic sugar for the binary term ... >>> such as philosopherand the prefix list representation of it. ... >>alternative Prolog notations for the same term: ... >>notation, the list notation, and the operator notation. ...
    (sci.logic)
  • Re: N-QUEENS problem with some differences
    ...     M is K-1, ... little different from Prolog. ... If the syntax for lists and "anonymous variables" ... squares and the position of queens as another ...
    (comp.lang.prolog)
Loading