Symbolic Functional Evaluation
TPHOLs '99: Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics(1999)
摘要
Symbolic functional evaluation (SFE) is the extension of an algorithm for executing functional programs to evaluate expressions in higher-order logic. SFE carries out the logical transformations of expanding definitions, beta-reduction, and simplification of built-in constants in the presence of quantifiers and uninterpreted constants. We illustrate the use of symbolic functional evaluation as a "universal translator" for linking notations embedded in higher-order logic directly with automated analysis without using a theorem prover. SFE includes general criteria for when to stop evaluation of arguments to uninterpreted functions based on the type of analysis to be performed. SFE allows both a novice user and a theorem-proving expert to work on exactly the same specification. SFE could also be implemented in a theorem prover such as HOL as a powerful evaluation tactic for large expressions.
更多查看译文
关键词
Model Check, Propositional Logic, Theorem Prover, Boolean Variable, Novice User
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要