没有合适的资源?快使用搜索试试~ 我知道了~
proof-search-ILLWiL:ILLWiL 论文的独立存储库
共110个文件
agda:86个
otf:6个
md:2个
需积分: 9 0 下载量 170 浏览量
2021-06-27
00:37:01
上传
评论
收藏 1.17MB ZIP 举报
温馨提示
ILLWiL 的证明搜索 Intuitionistic Linear Logic With Leftovers (ILLWiL) 是 Intuitionistic Linear Logic 的推广,具有弱化概念,非常适合通过构造证明搜索来纠正。 该存储库旨在以自包含的方式呈现论文“Certified Proof Search for Intuitionistic Linear Logic”中使用的材料。 目录树 equality/包含 Nils Anders Danielsson 库的子集的修补版本,用于“通过证明相关的成员关系进行袋等效”( , ),这是对我们的项目进行类型检查所必需的。 该允许我们同时使用他的库和标准库而不会发生冲突。 stdlib/包含对我们的项目进行类型检查所需的 Agda 标准库子集的副本。 它是从撰写本文时的最新稳定版本(即 0.9 版)中提取的。 lps
资源推荐
资源详情
资源评论
收起资源包目录
proof-search-ILLWiL:ILLWiL 论文的独立存储库 (110个子文件)
Equivalence.agda 56KB
Function-universe.agda 50KB
Equality.agda 47KB
Calculus.agda 36KB
Bag-equivalence.agda 28KB
RingSolver.agda 22KB
Closure.agda 22KB
Properties.agda 19KB
Equivalence.agda 19KB
BelongsTo.agda 18KB
Context.agda 17KB
Structures.agda 14KB
Tactics.agda 14KB
Algebra.agda 13KB
Binary.agda 12KB
Bijection.agda 12KB
Action.agda 11KB
Prelude.agda 10KB
List.agda 9KB
Linearity.agda 9KB
Decision-procedures.agda 8KB
Vec.agda 7KB
N-ary.agda 7KB
PropositionalEquality.agda 6KB
Nat.agda 6KB
Preimage.agda 6KB
Core.agda 6KB
Surjection.agda 6KB
Maybe.agda 6KB
Unary.agda 6KB
Fin.agda 6KB
Fin.agda 5KB
Operations.agda 5KB
AlmostCommutativeRing.agda 5KB
Lemmas.agda 5KB
Consumption.agda 5KB
H-level.agda 4KB
Decidable-UIP.agda 4KB
Consequences.agda 4KB
Reflection.agda 4KB
Equality.agda 4KB
Equivalence.agda 4KB
Examples.agda 3KB
Product.agda 3KB
Decidable.agda 3KB
Function.agda 3KB
Simple.agda 3KB
FunctionProperties.agda 3KB
Group.agda 3KB
Maybe.agda 3KB
Morphism.agda 2KB
IMLL.agda 2KB
Indexed.agda 2KB
Ring.agda 2KB
Core.agda 2KB
Groupoid.agda 2KB
Logical-equivalence.agda 2KB
Unit.agda 2KB
Indexed.agda 2KB
Injection.agda 2KB
Bool.agda 2KB
Injection.agda 2KB
PreorderReasoning.agda 2KB
AbelianGroup.agda 2KB
Sum.agda 2KB
Propositional.agda 1KB
Core.agda 1KB
EqReasoning.agda 1KB
Core.agda 1KB
Indexed.agda 1KB
Monad.agda 1KB
Nullary.agda 856B
Core.agda 818B
Core.agda 798B
Core.agda 724B
ProofSearch.agda 676B
Simple.agda 644B
Applicative.agda 634B
Nullary.agda 634B
Core.agda 580B
Functor.agda 548B
PartialOrderReasoning.agda 511B
Core.agda 487B
Level.agda 455B
Identity.agda 453B
Empty.agda 400B
main.bib 6KB
lipics.cls 23KB
.dropbox_uploader.enc 160B
.gitignore 10B
lps.lagda 80KB
lps-short.lagda 62KB
LICENCE 1KB
Makefile 132B
README.md 2KB
index.md 693B
xits-math.otf 518KB
xits-regular.otf 244KB
xits-mathbold.otf 243KB
xits-bold.otf 148KB
共 110 条
- 1
- 2
资源评论
CharlesXiao
- 粉丝: 13
- 资源: 4489
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功