如何解决Coq语法谓词逻辑
有人可以用coq语法帮我解决以下问题:
〜(存在x:D,〜R x)|-(全部y:D,R y)
解决方法
首先,您必须定义D和R,方法是预先定义D或R,或者使用量词将其定义在范围内。 蕴含通常通过Coq蕴涵(->)建模。
这将给出以下内容
forall (D : Prop) (R : D -> Prop),~ (exists x:D,~ R x) -> (forall y:D,R y).
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。