Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

First Order Logic (FOL) parsing

1,041 views
Skip to first unread message

Erotavl...@libero.it

unread,
Dec 7, 2010, 3:49:37 AM12/7/10
to
Hi All,

I'm new about the topic of parsing. I have to develop a parser/compiler for
First Order Logic (FOL) clauses in C/C++ language. I have made a lot of search
on the web but I have found only a source codes written in ML, PROLOG,
Haskell, Python, etc. I have also found a open source AI project that is
written in C/C++ which has a internal FOL parser developed with Bison. The
project is Alchemy http://alchemy.cs.washington.edu/. Do you know it? and what
do you think about it? It's better to try to use it or to rewrite a new
parser?

At the moment I'm studying Flex and Bison to understand how I can generate a
parser. I think it's a big work for me. Do you know if exist an open source
implementation (C/C++) from which I can start apart of Alchemy project?

I would like to know if a LALR parser is able to treat a FOL grammar or if I
need a GLR parser. What do you think?

Thank you

Hans Aberg

unread,
Dec 10, 2010, 2:27:13 PM12/10/10
to
On 2010/12/07 09:49, Erotavl...@libero.it wrote:
> I'm new about the topic of parsing. I have to develop a parser/compiler for
> First Order Logic (FOL) clauses in C/C++ language. I have made a lot of search
> on the web but I have found only a source codes written in ML, PROLOG,
> Haskell, Python, etc.

There is Otter
http://www.mcs.anl.gov/research/projects/AR/otter/index.html

And Qu-Prolog looked interesting (don't recall implementation language):
http://www.itee.uq.edu.au/~pjr/HomePages/QuPrologHome.html

Some other links:
http://www.mcs.anl.gov/research/projects/AR/others.html
http://en.wikipedia.org/wiki/Automated_theorem_proving

> At the moment I'm studying Flex and Bison to understand how I can generate a
> parser. I think it's a big work for me.

It depends on what you mean by "first order logic". If it involves
quantifiers that bind variables, that is a lot of tricky work to get it
correct. So it is best to settle on some library that can do that for
you, if such one exists.

If you merely want Prolog style free variables, then the Haskell
interpreter Hugs has a mini-Prolog example. I once translated it into C++.

As for getting started with Bison/Flex, try the C++ calculator example
in the Bison manual, which also comes in the distribution. Then it is
easy to rewrite it.

Gene

unread,
Dec 10, 2010, 10:27:14 PM12/10/10
to
On Dec 7, 3:49 am, Erotavlas_tu...@libero.it wrote:
> Hi All,
>
> I'm new about the topic of parsing. I have to develop a parser/compiler for
> First Order Logic (FOL) clauses in C/C++ language. I have made a lot of
search
> on the web but I have found only a source codes written in ML, PROLOG,
> Haskell, Python, etc. I have also found a open source AI project that is
> written in C/C++ which has a internal FOL parser developed with Bison. The
> project is Alchemyhttp://alchemy.cs.washington.edu/. Do you know it? and

what
> do you think about it? It's better to try to use it or to rewrite a new
> parser?
>
> At the moment I'm studying Flex and Bison to understand how I can generate a
> parser. I think it's a big work for me. Do you know if exist an open source
> implementation (C/C++) from which I can start apart of Alchemy project?
>
> I would like to know if a LALR parser is able to treat a FOL grammar or if I
> need a GLR parser. What do you think?

It should certainly be easy to parse any reasonable grammar for FOL
with a LALR(1) or LL(1) parser. For example if you translate the
description at http://www.sju.edu/~jhodgson/ugai/1order.html to Bison,
you get something like this

%token PREDICATE FUNCTION CONSTANT VARIABLE
%token IMPLIES AND OR IFF THERE_EXISTS FORALL
%left '='
%left VARIABLE
%left IMPLIES
%left IFF
%left AND
%left OR
%left NOT
%%

sentence
: atomic_sentence
| sentence IMPLIES sentence
| sentence IFF sentence
| sentence AND sentence
| sentence OR sentence
| quantifier VARIABLE sentence
| '~' sentence %prec NOT
| '(' sentence ')'
;
atomic_sentence
: PREDICATE '(' term_list ')'
| term '=' term
;
term
: FUNCTION '(' term_list ')'
| CONSTANT
| VARIABLE
;
term_list
: term_list term
| term
;
quantifier
: THERE_EXISTS
| FORALL
;

ranias...@gmail.com

unread,
May 3, 2015, 6:00:07 PM5/3/15
to
I want more examples of FOL in lex/bison and how o prove that it is
LL(1)or LALR

0 new messages