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

[Stephan Opfer]

Hi Antlr-Interest,

I think that my first order logic grammar is ready. I want to upload it
to the antlr grammar collection, if you don't protest, because of any
problem with the grammar.

Best Regards,
  Stephan

On 04/22/2012 09:57 AM, Stephan Opfer wrote:
> Hi JBB,
> 
> thank you for your help! The grammar you send look really nice and the
> "unnecessary changes" helped me to understand ANTLR a little bit more.
> 
> I am not sure, if I want the variable of the quantifier as sibling or
> parent of their scope. Maybe its more convenient to have something like this
> 
> Exists
>   |
>   V
>   ?x
>   |
>   V
> (formula)
> 
> , instead of the version you sent to me
> 
>        Exists
>   _______|_______
>  |               |
>  V               V
>  ?x          (formula)
> 
> I tried to achieve this, but failed, because of several
> NoViableAltExceptions. Before I head on to this, I first make the rest
> of the software run.
> 
> Best Regards,
>   Stephan
> 
> On 04/20/2012 10:08 PM, John B. Brodie wrote:
>> Greetings!
>>
>> Attached please find a tested (on just your single sample input string)
>> version with the quantifier at a higher precedence that the disjunctive
>> operation.
>>
>> Basically just moved the quantifier clause higher up in the rule set.
>>
>> And sorry but I also made a bunch of unnecessary gratuitous changes
>> along the way...
>>
>> Hope this helps...
>>    -jbb
>>
>> On 04/20/2012 10:37 AM, Stephan Opfer wrote:
>>> 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
>>>>>
>>>
>>> List: http://www.antlr.org/mailman/listinfo/antlr-interest
>>> Unsubscribe:
>>> http://www.antlr.org/mailman/options/antlr-interest/your-email-address
>>
> 
> 
> List: http://www.antlr.org/mailman/listinfo/antlr-interest
> Unsubscribe: http://www.antlr.org/mailman/options/antlr-interest/your-email-address
> 

-------------- next part --------------
grammar FOLFULv3;

options{
	language=Java;
	output=AST;
	ASTLabelType = CommonTree;
}

tokens{
	PREDICATE;
	FUNCTION;
}

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

condition: formula EOF! ;

formula	
	:	((FORALL^ | EXISTS^) VARIABLE)? disjunction ;

disjunction
	:	conjunction (OR^ conjunction)* ;

conjunction
	:	negation (AND^ negation)* ;

negation 
	:	NOT^? (predicate | LPAREN! formula RPAREN!) ;

predicate 
	:	PREPOSITION predicateTuple -> ^(PREDICATE PREPOSITION predicateTuple)
	| 	PREPOSITION ;

predicateTuple
	:	LPAREN! term (','! term)* RPAREN! ;

term	:	function | VARIABLE ;

function:	CONSTANT functionTuple -> ^(FUNCTION CONSTANT functionTuple)
	|	CONSTANT;

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

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

LPAREN : '(' ;
RPAREN :  ')' ;
AND :  '&' ;
OR :  '|' ;
NOT :  '!' ;
FORALL :  'Forall' ;
EXISTS :  'Exists' ;

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

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

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

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

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