hol-c
A proof-of-concept LCF-style interactive theorem prover for HOL(C)
Science Score: 54.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
✓Academic publication links
Links to: arxiv.org -
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (6.7%) to scientific vocabulary
Keywords
Repository
A proof-of-concept LCF-style interactive theorem prover for HOL(C)
Basic Info
Statistics
- Stars: 4
- Watchers: 2
- Forks: 1
- Open Issues: 2
- Releases: 0
Topics
Metadata Files
README.md
A modest proposal: explicit support for foundational pluralism
Introduction. This repo contains a basic Scala 3 implementation of an LCF-style interactive theorem prover for the HOL(C) logic introduced in the paper
A modest proposal: explicit support for foundational pluralism
by Dominic Mulligan and Martin Berger. The paper is available at arxiv.org/abs/2302.10137.
HOL(C) is a natural deduction presentation of HOL, but with a ternary judgement $\Gamma \vdash \phi : l$, adding a notion of taint $l$ to the more common binary judgements $\Gamma \vdash \phi$ between assumptions $\Gamma$ and formulae $\phi$. Taint can be seen as a kind of 'typing system' for proofs that explicitly tracks how classically or constructive a proof is, e.g. is $\phi$ deduced fom $\Gamma$ using Excluded Middle, or Reductio Ad Absurdum, or with Dependent Choice, or not? The purpose of this implementation is to serve as a proof-of-concept for fine-tuning the logic and for reviewing the paper. It is not intended to enable large-scale proof in HOL(C).
Compiling, testing and running the code. All relevant code is in
the src directory and can be compiled and executed with the scalac
compiler. The code is more easily used with sbt, using the provided
build.sbt file, by invoking
sbt compile
for compilation. Invoking
sbt test
executes a few property-based unit tests. Invoking
sbt run
executes integration tests, which are small theorems, including Peirce's law, proved using basic tactics.
Owner
- Name: Martin Berger
- Login: martinberger
- Kind: user
- Location: London
- Website: https://martinfriedrichberger.net
- Repositories: 3
- Profile: https://github.com/martinberger
Citation (CITATION.cff)
cff-version: 1.2.0 message: "If you use this software, please cite it as below." authors: - family-names: "Berger" given-names: "Martin" orcid: "https://orcid.org/0000-0003-3239-5812" - family-names: "Mulligan" given-names: "Dominic P." orcid: "https://orcid.org/0000-0003-4643-3541" title: "A modest proposal: explicit support for foundational pluralism" version: 0.2 doi: 10.48550/arXiv.2302.10137 date-released: 2023-02-20 url: "https://github.com/martinberger/hol-c"
GitHub Events
Total
- Push event: 3
Last Year
- Push event: 3
Issues and Pull Requests
Last synced: 6 months ago
All Time
- Total issues: 3
- Total pull requests: 2
- Average time to close issues: 6 days
- Average time to close pull requests: 4 minutes
- Total issue authors: 1
- Total pull request authors: 1
- Average comments per issue: 0.67
- Average comments per pull request: 0.0
- Merged pull requests: 1
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Issue authors: 0
- Pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
- martinberger (3)
Pull Request Authors
- martinberger (2)