首页 | 本学科首页   官方微博 | 高级检索  
     


Automated reasoning with function evaluation for COCOLOG
Authors:Suning Wang  Peter E. Caines
Affiliation:(1) Spar Aerospace Ltd., 21025 Trans‐Canada Highway, Ste‐Anne‐de‐Bellevue, Quebec, Canada, H9X 3R2;(2) Department of Electrical Engineering, McGill University, 3480 University Street, Montreal, P.Q., H3A 2A7, Canada;(3) Canadian Institute for Advanced Research, Canada
Abstract:The Conditional Observer and Controller Logic (COCOLOG) is a logical system for the feedback control of finite input‐state‐output systems wherein the individual first order logical theories have the properties of consistency, completeness and decidability. The efficiency of automatic theorem proving (ATP) is a crucial issue in the implementation of COCOLOG control systems and in this paper we present a so‐called function evaluation (FE) based resolution‐refutation ATP methodology for COCOLOG. FE‐resolution ATP replaces the axioms specifying the dynamics of a finite input‐state‐output machine by a set of defined function relations. The resulting procedure extends to predicates and hence permits the definition of constant and variable FE‐resolution inference. It is shown that FE‐resolution ATP is complete in the sense that a set of clauses which is unsatisfiable in all models with the given interpretation of the functions will yield the empty clause under resolution, paramodulation and FE‐resolution. This revised version was published online in June 2006 with corrections to the Cover Date.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号