Title :
Automated reasoning with function evaluation for COCOLOG with examples
Author :
Wang, Suning ; Caines, Peter E.
Author_Institution :
Spar Aerospace Ltd., Ste-Anne-de-Bellevue, Que., Canada
Abstract :
A function evaluation based automated (resolution) theorem proving (ATP) methodology is presented. It is called FE-resolution, for the sets of conditional observer and controller logics referred to by the acronym COCOLOG (conditional observer and controller logics). The unique model property of COCOLOG is presented, and the complete axiomatization and decidability properties of COCOLOG theories are given. The completeness of the FE-resolution method is proven, and complexity reduction via this technique is discussed. FE-resolution ATP is illustrated via a seven state machine example
Keywords :
decidability; function evaluation; inference mechanisms; observability; theorem proving; ATP; COCOLOG; FE-resolution; automated reasoning; automated theorem proving; axiomatization; completeness; complexity reduction; decidability; function evaluation; Aerospace control; Aerospace engineering; Automata; Automated highways; Automatic control; Automatic generation control; Calculus; Clocks; Control systems; Logic;
Conference_Titel :
Decision and Control, 1992., Proceedings of the 31st IEEE Conference on
Conference_Location :
Tucson, AZ
Print_ISBN :
0-7803-0872-7
DOI :
10.1109/CDC.1992.370957
