如何对伊莎贝尔/霍尔的变量(世界变化)的变化进行建模/形式化？
我试图在Isabelle/HOL中形式化业务规则，但是业务规则涉及一些变量的值的更改，比如if x=5 => x=6。=>不是通常的含义，因为x是一个世界中的5(解释、语义域)，在执行规则之后x是6，并且它已经是一个不同的世界(不同的解释、赋值函数、语义域)。因此，从技术上讲，is x=5 => x=6不是一阶逻辑的公式，也不是伊莎贝尔/霍尔的高阶逻辑公式。更有可能的是，它是动态/动作逻辑[rule1](x=5)=(x=6)中的公式(定义了当rule1应用于某些世界的公式时，在另一个世界中产生真实的公式(动态/动作逻辑本质上是一种模态逻辑，这里可以应用克里普克/可能的世界语义)。
现在，回到Isabelle/HOL或Coq: FOL/HOL理论是在所有世界或一个特定世界中的一组公式。如果我们停留在FOL/HOL，那么世界就没有变化，变量的值也没有变化。我们应该去模态逻辑，如果我们想要建模，理由为这样的变化。但这能在HOL中完成吗？这个世界的变化？
thesis.pdf是在Isabelle/HOL中对排序算法进行形式化化的一项很好的工作，在那里使用函数式编程，不需要变量，因此-不需要世界之间的这种变化。但是，如果我们试图在Isabelle/HOL中建模强化学习、马尔可夫过程、必要的/面向对象的编程、业务规则，那么我们就应该表达这种变化。怎么做？
如何在伊莎贝尔/霍尔中表达业务规则if x=5 => x=6？
在Coq中也可以使用同样的方法，这就是为什么Coq社区的答案也受到欢迎的原因。
回答 2
Stack Overflow用户
发布于 2020-07-03 06:45:38
最常见的解决方案是使用world => world => bool类型的谓词，表示世界或状态之间的转换(用于马尔可夫过程)或内存(用于程序验证)。它代表着从一个地方到另一个地方的过渡。
这样的谓词通常可以定义为表示非确定性的归纳谓词。
如果您对逻辑特别感兴趣：
- 对于伊莎贝尔来说，你可以看看它是如何在法新社的动态逻辑和模态逻辑的形式化中完成的(https://www.isa-afp.org/topics.html -搜索模态逻辑:在那页上)。
- 对于Coq，我已经找到了这个方法，它遵循相同的模式，但是还有许多其他的形式。
Stack Overflow用户
发布于 2020-07-03 08:18:39
我认为最直接的方法是为您的模态语言datatype fml = ...设置一个数据类型和一个满意谓词sat :: ('w ⇒ 'w ⇒ bool) ⇒ 'w ⇒ fml ⇒ bool，并将逻辑嵌入到Isabelle中。这(本质上)是徐和诺里什(徐先生的荣誉论文；IJCAR纸)所采取的方法。这种方法的缺点是它是一个深度嵌入，这意味着您必须自己处理变量绑定和替换。
您还可以使用typedecl和consts声明存在世界和可访问性关系，并将“解除连接词”定义为接受世界的函数，并返回布尔值，例如TT ≡ λw. True和◊φ ≡ λw. ∃v. (w R v) ∧ φ v ( R由consts定义)。这是Christophüller在这个G del本体论论点的预印中采取的方法。
https://stackoverflow.com/questions/62709073
复制相似问题
腾讯云开发者
