Syntax

PROGRAM 		 ::= 		   

moddecl 		 ::= 		  amodid [ [paramlist] ]
                 [modoper modexpr]
                 [ modexpr]

paramlist 		 ::= 		 paramlist  paramlist    
                    amodid modoper modexpr

modoper 		 ::= 		           

modexpr 		 ::= 		 bodyexpr modoper modexpr     bodyexpr

bodyexpr 		 ::= 		  decl 
            pathid [ [iparamlist] ]

iparamlist 		 ::= 		 modexpr  iparamlist    
                    modexpr

pathid 		 ::= 		 amodid     amodidpathid

decl 		 ::= 		 [hierarchy] [interface] [deductive] [control]

hierarchy 		 ::= 		 moddecl
             modid
             bodyexpr
            hierarchy hierarchy

interface 		 ::= 		 [ predicateidlist] 
                   [ predicateidlist]

predicateidlist 		 ::= 		 predid  predicateidlist     
predid

deductive 		 ::= 		 

    		 		 [ [   ]
          ]

    		 		 [   ]

    		 		 [ logcomp]

    		 		 

typebinding 		 ::= 		 typeid [ typespec]

typespec 		 ::= 		          
                           

     		 		 
      char-funct      symbollist       valuesspec      
      typeid

symbollist 		 ::= 		 symbol  [string]    
        symbollist  symbollist

valuesspec 		 ::= 		 symbol  [string] char-funct    
        valuesspec  valuesspec

char-funct 		 ::= 		  number 
       number  number  number 

predicate 		 ::= 		 predid  attributes

attributes 		 ::= 		 [name] [question] type [function] [  ]
                    [explanation] [image]

name 		 ::= 		  string

question 		 ::= 		  string

type 		 ::= 		  typespec

function 		 ::= 		    S-expression 

S-expression 		 ::= 		 atom     list     predef-func    
S-expression S-expression

list 		 ::= 		  S-expression        

predef-func 		 ::= 		   predid     
                       

relation 		 ::= 		  relationid pathpredid

pathpredid 		 ::= 		 pathidpredid     predid

relationid 		 ::= 		      
                          

     		 		       
                  
                  symbol

explanation 		 ::= 		  string

image 		 ::= 		  fileid

rule 		 ::= 		 ruleid  premisse-rule 
                          conclusion-rule [documentation]

premisse-rule 		 ::= 		 condition-rule  premisse-rule    
                        condition-rule

condition-rule 		 ::= 		 conditio       conditio 

conditio 		 ::= 		 operator  expression ... expression    

             		 		 expression operator expression   

             		 		 pathpredid     ltermid     
                                     

expression 		 ::= 		 operator-arit  expression ... 
                          expression    

              		 		  expression operator-arit expression    

              		 		 number     pathpredid

operator 		 ::= 		               
                                 

operator-arit 		 ::= 		                

conclusion-rule 		 ::= 		  rconclusion  cert-value

rconclusion 		 ::= 		 predid    
                 predid  symbol    
              predid     
                   predid  symbol 

logcomp 		 ::= 		 [lingtermdef] [conjunction] [renaming]

lingtermdef 		 ::= 		   ltermidlist 

ltermidlist 		 ::= 		 ltermid  ltermidlist     ltermid

conjunction 		 ::= 		   truth-table

truth-table 		 ::= 		   arrows 

arrows 		 ::= 		          arrows arrows

renaming 		 ::= 		    

lrenames 		 ::= 		 pathidltermid  cert-value

cert-value 		 ::= 		 ltermid    
           ltermid  ltermid 

control 		 ::= 		 

   		 		 [ evaltype]

   		 		 [ ltermid]

   		 		 [deduccnt] [structcnt]

 		 		 

evaltype 		 ::= 		           

deduccnt 		 ::= 		    

mrr 		 ::= 		 metaid  premisse-meta    

premisse-meta 		 ::= 		 mexpr  premisse-meta
                mexpr

filter-mrr 		 ::= 		  [relation-id] pathpredid   

            		 		  pathpredid      gexpr
                           known

structcnt 		 ::= 		    

mre 		 ::= 		 metaid  premisse-meta  filter-mre

filter-mre 		 ::= 		       

          		 		      cert-value   

          		 		   term        term 
                         amodid 

mrx 		 ::= 		 metaid  premisse-meta  exception

exception 		 ::= 		  predid   

          		 		 

mexpr 		 ::= 		 known     mrel     msubmod     mthres     card    
              atom     member   

        		 		 eqdif     moper     int    
              setof     pos     gexpr

symorvar 		 ::= 		 symbol     symbol

vpath 		 ::= 		 symorvar     symorvarvpath

known 		 ::= 		   fact, interval 

fact 		 ::= 		 factex      factex      
              listlist 

factex 		 ::= 		 vpath      vpath, symorvar 

interval 		 ::= 		 symbol 
                   symorvar, symorvar 

mrel 		 ::= 		 relationid symorvar, vpath 

msubmod 		 ::= 		  symorvar, symorvar     
                   symorvar 

mthres 		 ::= 		  symorvar, symorvar     
                   symorvar 

card 		 ::= 		  list, symorvar 

list 		 ::= 		 listid      listelem 

listelem 		 ::= 		 elemid     elemid  listelem

atom 		 ::= 		  list 

member 		 ::= 		   symorvar, list 

eqdif 		 ::= 		  listorsym,listorsym      
                listorsym,listorsym 

listorsym 		 ::= 		 symbol     list

moper 		 ::= 		 loper symorvar,symorvar 

loper 		 ::= 		                     
                    

int 		 ::= 		  list,list 

setof 		 ::= 		 
                      var,term,var 

pos 		 ::= 		  symorvar,list,symorvar 

gexpr 		 ::= 		 predid  term
                          ...  term 

term 		 ::= 		 varid     symbol    
               termid(term, ..., term)