%{
%}


%token Klammer_auf Komma Klammer_zu Trenner Gleich EOF
%token Negation Konjunktion Disjunktion Implikation Allquantor Existenzquantor
%token <...> Symbol

%type <...> term
%type <...> argumente
%type <...> satz formel infixfreie_formel
%type <...> konjunktion disjunktion
%type <...> saetze

%start saetze


%%


argumente :
    term                 {}
  | term Komma argumente {}
  ;

term :
    Symbol                                  {}
  | Symbol Klammer_auf argumente Klammer_zu {}
  ;

formel :
    konjunktion       {}
  | disjunktion       {}
  | implikation       {}
  | infixfreie_formel {}
  ;

infixfreie_formel :
    Symbol                                   {}
  | Symbol Klammer_auf argumente Klammer_zu  {}
  | term Gleich term                         {}
  | Klammer_auf formel Klammer_zu            {}
  | Negation infixfreie_formel               {}
  | Allquantor Symbol infixfreie_formel      {}
  | Existenzquantor Symbol infixfreie_formel {}
  ;

konjunktion :
    infixfreie_formel Konjunktion infixfreie_formel {}
  | infixfreie_formel Konjunktion konjunktion       {}
  ;

disjunktion :
    infixfreie_formel Disjunktion infixfreie_formel {}
  | infixfreie_formel Disjunktion disjunktion       {}
  ;

implikation :
    infixfreie_formel Implikation infixfreie_formel {}
  | infixfreie_formel Implikation implikation       {}
  ;

satz : formel Trenner {}

saetze :
    satz EOF    {}
  | satz saetze {}
  ;


%%