An experimental logic based on the fundamental deduction principle (Q580998)

The author describes an automatic deductive system SYMEVAL, without unification, and its applications to various scientific disciplines: set theory, logic programming, natural language analysis, program verification, inductive reasoning. SYMEVAL applies rules, axioms and definitions by replacing expressions by logically equivalent expressions (Fundamental Deduction Principle FDP). The deduction step encodings have the general form \(C\to P=Q\). SYMEVAl uses a logic for expressing logical axioms and the INTERLISP language for expressing rules. The logic satisfies the FDP, treats universal and existential quantifiers in analogous manner and is based on the elimination of quantifiers. The system uses a technique of reducing the scope of quantifiers in order to eliminate them.