Data

Tools

Indexes

Applications

Experiments

Open Source Science

prism

The proofs in Isabelle HOL of the PRISM theory.

https://github.com/ci-cse/prism

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 (8.3%) to scientific vocabulary
Last synced: 10 months ago · JSON representation ·

Repository

The proofs in Isabelle HOL of the PRISM theory.

Basic Info
  • Host: GitHub
  • Owner: CI-CSE
  • License: mit
  • Language: Isabelle
  • Default Branch: main
  • Size: 516 KB
Statistics
  • Stars: 1
  • Watchers: 2
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created over 1 year ago · Last pushed over 1 year ago
Metadata Files
Readme License Citation

README.md

PRISM

Programming really is simple mathematics.

This contains of some Eiffel implementation and Isabelle proofs for PRISM. The eiffel code is work in progress the isabelle files too but the theory is synchronized with the research paper. All definitions and claims have the same name in the isabelle files as they have in the reasearch paper.

Prerequisite

Default Isabelle2024 installation

How to use

Validate the proofs:

  1. Download this repository.
  2. And open the PRISM.thy file.
  3. In the Theories tab you see the progress of the validation.

Find proof

Use your prefered search engine for looking through multiple files or just search here on GitHub.

Prove a new claim

First state the claim at the end of PRISM.thy e.g. theorem "(p;q);r=p;(q;r)" - If the system tells you "Auto solve_direct: the current goal can be solved directly with..." in which case we already proved the property. - Else you can ask Sledgehammer to solve it and it will produce something like cvc4 found a proof... Try this: by simp - If Sledgehammer does not find a proof you have to learn a bit of Isabelle and prove it manually.

Owner

  • Name: Constructor Institute - Chair of Software Engineering
  • Login: CI-CSE
  • Kind: organization

Citation (CITATION.cff) 

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: "Weber"
  given-names: "Reto"
  orcid: "https://orcid.org/0009-0001-9262-4843"
title: "PRISM proofs"
version: 1.0.0
date-released: 2025-02-20
url: "https://github.com/CI-CSE/PRISM"

GitHub Events

Total
  • Watch event: 3
  • Push event: 9
  • Create event: 3
Last Year
  • Watch event: 3
  • Push event: 9
  • Create event: 3