Re: FOL, ZFC, NGB and Prolog

Barb Knox wrote:

> The issue here isn't about computational power but about expressiveness.

I see (these terms are not synonymous).

> For example, there is no direct Prolog translation of this FOL:
> Ax (P(x) v Q(x))

I see.

> For another example, Prolog's negation-as-failure means that Prolog a model
> of some domain relies on the "closed world assumption": if you can't prove
> that something is true then it must be false. This is different from full
> FOL.

Thank you very much for another kind and meaningful comment, Ms Knox.
As it usually happens with my comprehending your comments, I will
understand this one after a long while of pondering its contents. I
will try to excuse myself by saying that I have only recently came
accross the idea of interpreting FOL computationally (i.e. on a
register machine through a metacircular Prolog compiler) and still have
almost no experience in using Prolog. Would you be kind enough as to
suggest where to start?

Surely there is:

http://www.swi-prolog.org/ as well as
http://www.ida.liu.se/~ulfni/lpp/ and also
http://swiss.csail.mit.edu/classes/6.001/abelson-sussman-lectures/ for
a Lisp variant of a functional language.

Still, it would be lovely to study some educational material geared
particularly towards implementing some variant of FOL in Prolog, or
several of such variants with plenty of comments (say the
Hilbert-Ackerman system and the system of PM). Please, is there a
relevant internet resource (perhaps also discussing ZFC and putting all
of the material into the light of bare pattern matching)?

Thank you very much again for your patience, Ms Knox.

Kindest regards,
Tom

---------------------------
| BBB b \ Barbara at LivingHistory stop co stop
uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------

.

Relevant Pages

  • Re: predicate in a predicate
    ... Prolog is somehow from Horn Clauses, they can have at most one ... how can I convert the FOL that have two positive ... With negation as failure you can go beyond horn clauses. ...
    (sci.logic)
  • Re: predicate in a predicate
    ... Prolog is somehow from Horn Clauses, they can have at most one ... how can I convert the FOL that have two positive ... With negation as failure you can go beyond horn clauses. ... positivity check is ok, so this amounts to prolog as: ...
    (sci.logic)
  • Re: FOL, ZFC, NGB and Prolog
    ... >> Tom wrote: ... Prolog is much more restrictive than FOL. ... Prolog, like all reasonable programming languages, is Turing complete. ...
    (sci.logic)
  • Re: FOL, ZFC, NGB and Prolog
    ... >> Tom wrote: ... >>> merely, FOL in executable notation. ... Prolog is much more restrictive than FOL. ...
    (sci.logic)