文件名称：semantic-query:语义查询优化
文件大小：443KB
文件格式：ZIP
更新时间：2024-05-19 15:27:42
TeX
语义查询 该存储库演示了使用追逐算法的语义查询优化。 有两种实现。 基于战术的（在LtacChase.v中实现） 在Chase.v中实施的Gallina一号 两者具有不同的权衡。 Ltac的实现可以重复利用Coq的丰富知识，例如congruence和omega ，以消除附带条件。 因为它重用了Coq的内部表示，所以它还可以支持更有趣的绑定结构，例如嵌套关系。 Ltac实施的缺点是，与基于Gallina的实施相比，它的运行速度非常慢，尤其是在最小化的情况下，必须对候选人进行回溯以确定等同性。
【文件预览】：
semantic-query-master
----.gitignore(83B)
----README.md(746B)
----theories()
--------ShallowTableaux.v(660B)
--------RecordTableaux.v(15KB)
--------ChaseShallow.v(4KB)
--------PredModel.v(3KB)
--------Chase.v(16KB)
--------Demo.v(6KB)
--------LtacChase.v(21KB)
--------Tables.v(732B)
--------DemoLtacMovies.v(4KB)
--------Expr.v(20KB)
--------HomomorphismSearch.v(14KB)
--------InductiveTableaux.v(708B)
--------Entailer.v(3KB)
--------DataModel.v(11KB)
--------ProveED.v(3KB)
--------Minimize.v(4KB)
--------Parsing.v(8KB)
--------DemoLtacIndex.v(4KB)
--------ListModel.v(10KB)
--------Types.v(2KB)
----LICENSE(1KB)
----_CoqProject(473B)
----paper()
--------.gitignore(53B)
--------sigplanconf.cls(38KB)
--------lstcoq.sty(6KB)
--------thesisbib.bib(131KB)
--------coqsem.tex(99KB)
--------ucsd.png(312KB)
--------Makefile(245B)
--------slides.tex(21KB)
--------mit.png(4KB)
----Makefile(175B)