我正在寻找一个工具(首选GUI但CLI可以工作),它允许我输入数学表达式,然后执行它们的操作,但限制我只有数学上有效的操作.此外,该工具必须能够保存会话,然后证明给定的已保存操作集是有效的.
注意:我不是在寻找一个生成校样的系统,只是检查我手动指定的步骤是否有效.
我已经使用ACL2进行类似的操作,并且它在某些情况下表现很好但是很难用于其他所有情况.
这个小项目是我的动力.它是一种D模板类型,允许求解方程.鉴于这个等式:
(A * B) = C + D / F;
可以将任何一个符号设置为未知,并评估该表达式将导致对该变量的赋值.它的工作原理是将表达式树构建到类型中,然后使用重写规则将其转换为可以针对未知类型进行事件处理的事物.
我需要的是一些验证重写规则的方法.可以通过测试给定某种关系为真的断言来验证它们,另一种也是.
我有定义的归纳类型:
Inductive InL (A:Type) (y:A) : list A -> Prop :=
| InHead : forall xs:list A, InL y (cons y xs)
| InTail : forall (x:A) (xs:list A), InL y xs -> InL y (cons x xs).
Inductive SubSeq (A:Type) : list A -> list A -> Prop :=
| SubNil : forall l:list A, SubSeq nil l
| SubCons1 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq l1 (x::l2)
| SubCons2 : forall (x:A) (l1 …在COQ中,类型prod(具有一个构造函数对)对应于笛卡尔积和类型sig(存在一个构造函数)对依赖和,但是如何描述笛卡尔积是特定的依赖和的情况？我想知道prod和sig之间有一个联系,例如一些定义相等但我在参考手册中没有明确地找到它.
自动证明两个一阶公式 F 和 G 等价的最佳方法是什么？
与“完整”一阶公式相比，这些公式有一些限制：
我可以将这些公式转换为子句范式，并且我有统一文字的例程。但是我不确定如何继续以及这个问题是否可以解决。