文件名称：Qed:具有内置理论的一阶逻辑库
文件大小：116KB
文件格式：ZIP
更新时间：2024-05-03 13:20:38
OCaml
:warning: 过时的存储库 :warning: Qed的开发现已与Frama-C在一起。 具有理论的一阶逻辑 Qed是一个库，它使用内置的理论来实现一阶逻辑。 它由CEA-Tech在Sofware可靠性和安全性实验室中开发，并随附于平台，用于通过最弱前提条件（WP）证明ACSL合同。 该库的设计在NASA上发表的文章“ [已答：计算仍待证明的内容]（ ）”中进行了描述。正式方法，2015年。 该库的主要功能是： 布尔理论 量词 整数理论和实数论 排列并记录理论 未解释的函数，由关联，可交换性，中性和吸收剂，内射性，构造函数和可逆性扩展 可扩展的重写器，用于解释功能 完全标准化的词语WRT理论 用于记忆，替换，共享子术语的组合器 灵活的漂亮印刷 将引擎导出到SMT求解器和校对助手 安装 要求： ocaml 4.04或更高版本，带有ocamlfind和ocamlbuild 要构建和安装该库，请执行以下
【文件预览】：
Qed-master
----.ocp-indent(17B)
----licenses()
--------ceatech.css(3KB)
--------LGPLv2.1(24KB)
--------header.config(262B)
--------HEADER(645B)
----frama-c.sh(644B)
----qed.opam(520B)
----.gitlab-ci.yml(311B)
----CONTRIBUTING.md(53B)
----src()
--------partition.mli(3KB)
--------idxmap.ml(6KB)
--------hcons.mli(3KB)
--------listmap.mli(3KB)
--------intset.ml(3KB)
--------collection.ml(5KB)
--------intmap.ml(28KB)
--------pool.ml(4KB)
--------collection.mli(5KB)
--------mergeset.mli(3KB)
--------mergemap.ml(5KB)
--------bvars.mli(3KB)
--------intmap.mli(4KB)
--------plib.mli(4KB)
--------kind.mli(3KB)
--------export_coq.ml(15KB)
--------listset.mli(3KB)
--------export_why3.mli(3KB)
--------listmap.ml(10KB)
--------idxset.ml(4KB)
--------term.ml(81KB)
--------jbuild(128B)
--------mergemap.mli(4KB)
--------idxset.mli(3KB)
--------term.mli(3KB)
--------export_altergo.ml(15KB)
--------engine.ml(10KB)
--------pool.mli(2KB)
--------pretty.ml(17KB)
--------export.ml(36KB)
--------mergeset.ml(4KB)
--------partition.ml(4KB)
--------hcons.ml(4KB)
--------cache.mli(2KB)
--------logic.ml(15KB)
--------export_why3.ml(12KB)
--------pretty.mli(2KB)
--------idxmap.mli(3KB)
--------bvars.ml(3KB)
--------intset.mli(2KB)
--------export.mli(6KB)
--------cache.ml(3KB)
--------export_whycore.ml(9KB)
--------export_altergo.mli(3KB)
--------listset.ml(7KB)
--------export_whycore.mli(6KB)
--------export_coq.mli(3KB)
--------plib.ml(7KB)
--------kind.ml(8KB)
----LICENSE.md(188B)
----.gitignore(42B)
----CHANGELOG.md(282B)
----Makefile(3KB)
----README.md(1KB)
----.oci(258B)