CENTAUR: the system

syntax terms occur in most rules. They have to be valid terms w.r.t. their abstract syntax. Every such term is typed with a syntatic category. The type-checking phase of TYPOL compilation uses this information in verifying a TYPOL specification and generates an intermediate form. The output from the type-checking phase can be plugged into several code generators. Currently we use a Prolog code generator written in TYPOL. Here we take advantage of the similarity between Prolog variables and variables in inference rules. Roughly speaking, the denominator of a rule maps to a clause head and the premises to the clause body. Given a semantic specification we want to use the computer to solve various equations. Typical unknowns are values, types, states, etc. An equation is turned into a Prolog goal which is then solved by the Prolog interpreter. 4.3. Operating the logical engine The TYPOL compiler generates Prolog code. To use this code from CENTAUR, a goal must be constructed and mailed t..