Title :
Recognition of normal forms with tree automata for inductive theorem proving
Author :
Sato, Hikaru ; Kurihara, Masazumi
Author_Institution :
Grad. Sch. of Inf. Sci. & Technol., Hokkaido Univ., Sapporo, Japan
Abstract :
In this paper, we propose a method to construct a tree automata which recognizes all ground normal forms of a given term with respect to a terminating and confluent constructor TRS. We also show that the technique can be applied for generalization of conjecture in inductive theorem proving.
Keywords :
automata theory; theorem proving; inductive theorem proving; normal form recognition; tree automata; Automata; Cognition; Computer science; Context; Educational institutions; Equations; Reactive power; Equational reasoning; Formal verification; Inductive theorem proving; Term rewriting systems;
Conference_Titel :
Science and Information Conference (SAI), 2013
Conference_Location :
London
