The authors present a resolution method from a first order predicate logic formula F(x,y) into a function f as its executable code which computes y from x regarding x as the inputs and y as the outputs. A resolution process of the form For all z G(x,y,z) is argued in particular. This method can be regarded as a theorem proving method for first order predicate logic formulae. From the point of view, the resolution would be the theorem proving of the form ' For all x There exists y For all z G(x,y,z)'. The function f is generated by means of the application of the pre-defined rules. These rules can be classified into two groups; transformation rules and resolution rules. The former rules transform a logic formula itself, and the latter rules resolve a function and/or a function definition. The latter rules are applied first if possible. If no latter rules can be applied, then the former transformation rules are applied. The paper briefly describes some example of the resolution process and verification of its partial correctness.
展开▼
