Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

L

LATIN2
- Activity
- Members
- Labels
- Issues
- Issue boards
- Milestones
- Iterations
- Wiki
- Requirements
- Environments
- Terraform modules
- Incidents

Snippets Groups Projects

f174106f

Verified Commit f174106f authored 1 year ago by ColinRothgang

Downloads
- Patches
- Plain Diff

Add results of running HOL ATPS on category theory lemmas in DHOL vs native HOL

parent 1bf59a83

No related branches found

No related tags found

No related merge requests found

Changes 8

Expand all Hide whitespace changes

Inline Side-by-side

Showing

scala/latin2/tptp/DIHOLExporter.scala 1 addition, 1 deletion

scala/latin2/tptp/DIHOLExporter.scala
scala/latin2/tptp/HOLExporter.scala 1 addition, 2 deletions

scala/latin2/tptp/HOLExporter.scala
source/casestudies/2023-cade/MMT_example_problems/cat.mmt 47 additions, 22 deletions

source/casestudies/2023-cade/MMT_example_problems/cat.mmt
source/casestudies/2023-cade/MMT_prover_output/$Cat$Extended$H$O$L.ax 34 additions, 0 deletions

...tudies/2023-cade/MMT_prover_output/$Cat$Extended$H$O$L.ax
source/casestudies/2023-cade/MMT_prover_output/$Cat$Extended.ax 15 additions, 2 deletions

.../casestudies/2023-cade/MMT_prover_output/$Cat$Extended.ax
source/casestudies/2023-cade/MMT_prover_output/$Cat$Extended.p 25 additions, 0 deletions

...e/casestudies/2023-cade/MMT_prover_output/$Cat$Extended.p
source/casestudies/2023-cade/extended-category-theory-dhol-vs-native-hol-results-comparison.txt 252 additions, 0 deletions

...category-theory-dhol-vs-native-hol-results-comparison.txt
source/casestudies/2023-cade/test-mmt-based-prover.msl 3 additions, 0 deletions

source/casestudies/2023-cade/test-mmt-based-prover.msl

with 378 additions and 27 deletions

Loading

0% Loading or .

You are about to add 0 people to the discussion. Proceed with caution.

Finish editing this message first!

Please register or sign in to comment