我想在 Isabelle 中创建一个函数 F，给出一个公式
formula = pr int | neg formula | imp formula formula
如果公式是重言式，则产生 True，否则产生 False。
例如：
F( φ ⇒ φ ) = True
F( φ ⇒ (ψ ⇒ φ) ) = True
F( ψ ⇒ φ ) = False
任何人都可以帮助我？我发现很难理解 Isabelle 的文档，我找不到这样的功能（我认为它应该已经存在）。
0
在任何情况下，如果您想谈式的重言式（或公式的任何语义属性），您首先需要为公式定义语义，即函数eval :: formula ⇒ (int ⇒ bool) ⇒ bool（假设pr构造函数表示自由变量）接受公式和变量赋值，并返回公式是否适用于该赋值。
您可以通过使用primrec或fun命令对公式进行递归来定义这样的函数。Isabelle 网站上的‘Programming and Proving‘ tutorial有很多示例。
本站系公益性非盈利分享网址，本文来自用户投稿，不代表码文网立场，如若转载，请注明出处
评论列表（13条）