# [antlr-interest] Grammar for Predicate Logic (FOL)

Stephan Opfer stephan.opfer at gmx.net
Fri Apr 20 07:37:53 PDT 2012

```Hi,

I think I created a grammar, which accepts prepositional logic and first
order logic. the only problem I see at the moment, is that quantifiers
are not the parent, but siblings of their scope.

I have an example input:

Exists ?x (Forall ?y Check(?y) & HasRelation(?x, ?y)) & (Exists ?y
NoCheck(?y) & HasNoRelation(?x, ?y))<EOF>

Exists ?x is a sibling of the & between the parenthesed formulas, but I
want ?x to be parent of this &. The problem is at the second alternative
of the element rule. Here is the grammar:

grammar FOLFUL;

options{
language=Java;
output=AST;
}

tokens{
LPAREN='(';
RPAREN= ')';
AND= '&';
OR= '|';
NOT= '!';
FORALL= 'Forall';
EXISTS= 'Exists';
}

/*------------------------------------------------------------------
* PARSER RULES
*------------------------------------------------------------------*/

condition: formula EOF!;

formula: conjunction (OR^ conjunction)*;

conjunction: element (AND^ element)*;

element	: NOT^? atom
| NOT^? quantifier formula
| NOT^? LPAREN! formula RPAREN!
;

quantifier : (FORALL^ | EXISTS^) VARIABLE;

atom 	: PREPOSITION^ tuple?;

tuple	: LPAREN! (CONSTANT | VARIABLE) (','!(CONSTANT | VARIABLE))* RPAREN! ;

/*------------------------------------------------------------------
* LEXER RULES
*------------------------------------------------------------------*/

VARIABLE: '?' (('a'..'z') | ('0'..'9')) CHARACTER*;

CONSTANT: (('a'..'z') | ('0'..'9')) CHARACTER*;

PREPOSITION: ('A'..'Z') CHARACTER*;

CHARACTER: ('0'..'9' | 'a'..'z' | 'A'..'Z' | '_');

WS : (' ' | '\t' | '\r' | '\n')+ {\$channel = HIDDEN;};

Best Regards,
Stephan

On 04/19/2012 11:37 PM, Stephan Opfer wrote:
> Oh! Thanks Jim! That was easy :)
>
> On 04/19/2012 11:16 PM, Jim Idle wrote:
>> language=Java; // Case sensitive.
>>
>> Jim
>>

```