GENTZEN SYSTEM CALCULUS IMPLEMENTATION FOR SYMBOLIC MINIMALIZATION OF COMPLICATED LOGICAL EXPRESSIONS

The paper presents a practical application of Gentzen theorem proving system by means of an experimental computer tool, for the purpose of logic expressions normalization into the form similar to the Horn clauses. The initial expressions are described as complicated nested condition rules in general rule-based form “IF THEN”. Additionally the paper describes a particular kind of logic algorithms optimization and some possibilities of increasing of efficiency of the presented application, for the normalizing a great number of symbolic expressions.