Decidability of the Class E by Maslov's Inverse Method

摘要

We present a simple formulation of S. Maslov's inverse method of proof (and proof search) for first order predicate logic and illustrate it by proving decidability of validity for formulas with one existential quantifier and arbitrary function symbols.