Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

First draft for interactive theorem provers #14

Open
wants to merge 6 commits into
base: trunk
Choose a base branch
from
Open

First draft for interactive theorem provers #14

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cb607d9
real init
rinshankaihou Nov 20, 2019
237e7b9
almost
rinshankaihou Nov 21, 2019
364a6f9
todo fix citation
rinshankaihou Nov 21, 2019
ef81460
basically done; need to check grammer
rinshankaihou Dec 3, 2019
d713498
second draft
rinshankaihou Dec 4, 2019
2ef50dd
final draft
rinshankaihou Dec 17, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/itp.bib
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
@inproceedings{klein09,
author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
title = {seL4: Formal Verification of an OS Kernel},
booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
title = {seL4: Formal Verification of an {OS} Kernel},
booktitle = {Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles},
series = {SOSP '09},
year = {2009},
pages = {207--220},
Expand Down Expand Up @@ -51,7 +51,7 @@ @article{quaresma17
}

@article{braun17,
title={A synthetic proof of Pappus’ theorem in Tarski’s geometry},
title={A synthetic proof of {Pappus}’ theorem in {Tarski}’s geometry},
author={Braun, Gabriel and Narboux, Julien},
journal={Journal of Automated Reasoning},
volume={58},
Expand All @@ -71,7 +71,7 @@ @article{narboux07
}

@inproceedings{boutry16,
title = {From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry},
title = {From {Tarski} to {Descartes}: Formalization of the Arithmetization of Euclidean Geometry},
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"Euclidean" should also be capitalized

author = {Boutry, Pierre and Braun, Gabriel and Narboux, Julien},
booktitle={the 7th International Symposium on Symbolic Computation in Software Science},
year = {2016},
Expand All @@ -86,15 +86,15 @@ @incollection{aspinall07
}

@inproceedings{lerner15,
title={Polymorphic blocks: Formalism-inspired UI for structured connectors},
title={Polymorphic blocks: Formalism-inspired {UI} for structured connectors},
author={Lerner, Sorin and Foster, Stephen R and Griswold, William G},
booktitle={Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems},
pages={3063--3072},
year={2015},
}

@inproceedings{aspinall00,
title={Proof General: A generic tool for proof development},
title={{Proof General}: A generic tool for proof development},
author={Aspinall, David},
booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
pages={38--43},
Expand Down
36 changes: 21 additions & 15 deletions src/itp.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,25 +4,25 @@

Overview
========
Formal verification is essential to make sure important properties such as safety hold in software or hardware systems.



:cite:`klein09` Complete formal verification is the only known way to guarantee that a system is free of programming errors.
"Complete formal verification is the only known way to guarantee that a system is free of programming errors." :cite:`klein09`

Important applications of formal verification include: aerospace softwares such as those who prevent airplane collision;
microprocessor producers such as Intel have their own verification team; there are also works about the
language Rust, which, though haven't been completely verified, provides safety and performance at the same time.
microprocessor producers such as Intel have their own verification team.
A cryptographic system must ensure that its protocol is error free, while the errors are hard to notice.

An interactive theorem prover (ITP), sometimes refered to as proof assistant, is a programming environment that helps
humans to write formal proofs. In contrast to automated theorem provers, ITPs require human guidance,
though they also have a certain level of automation power.
Different to a traditional proof conducted through a pen-and-paper approach, a formal proof conducted by computers
is completely rigorous, and is oftenly tedious and hard.
is completely rigorous, and is oftenly tedious and hard. Similarly, a machine proof is usually cumbersome as well.
For example, seL4, a verified microkernel that we will mention later, takes a total of about 23 person years for its
development of framework, libraries and functional correctness proof, and those sums up to 200,000 lines of code in the ITP Isabelle. :cite:`klein09`

It is worth noting that, usually we treat the theorem prover as a trusted computing base (TCB). In other words, we have to trust the theorem provers.

It is worth noting that, when we say some formal proof done by a theorem prover works,
we impose the implicit assumption that the theorem prover is error-free. In other words, we have to trust the theorem provers.


Notable Computer-Aided Proofs
Expand Down Expand Up @@ -55,7 +55,8 @@ Notable Computer-Aided Proofs

Gamification
============
There are several interesting works for gamification, one of them is `Polymorphic Blocks <https://cseweb.ucsd.edu/~lerner/pb.html>`_ .
Gamification of ITPS is translating them into games.
Check out one of them: `Polymorphic Blocks <https://cseweb.ucsd.edu/~lerner/pb.html>`_ .

.. container:: bib-item

Expand All @@ -79,8 +80,12 @@ There are several interesting works for gamification, one of them is `Polymorphi
whether it helps the user understand the symbolic meaning of the formulas. The paper also states that this tool has a potential of
laying the foundation for crowdsourcing proofs via gamification.

Proof General
Unifying ITPs
=============
There are many different ITPs, and an extension for one of them
does not easily transport to another. Proof General, a canonical IDE for ITPs,
is a framework that tackles this problem.

.. container:: bib-item

.. bibliography:: itp.bib
Expand All @@ -100,13 +105,14 @@ Proof General


Now there are `more features, <http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual&file=releases%2FProofGeneral%2Fdoc%2FProofGeneral%2FProofGeneral_2.html>`_
supported by proof general, such as proof by pointing (appropraite tactics or lemmas are automatically applied
supported by proof general, such as proof by pointing (appropriate tactics or lemmas are automatically applied
when clicking on a subterm of a goal) and proof-tree visualization.


Geometry Interactive Theorem Prover (GTP)
=========================================

Geometry Interactive Theorem Provers (GTP) are used for proving geometric properties.

GTPs has potential for education.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is GTP? You need to introduce the topic before saying it has potential for education.

This book describes a possible direction of developing GTP:
Expand Down Expand Up @@ -139,7 +145,7 @@ Let us look at a substantial example.
The geometry software is used for drawing geometric figures and inventing conjectures by using feed back from the geometric software
, and a theorem prover is used to prove the conjectures.
In the automatic mode, the conjecture along with the graph created by the user is rewritten and translated to the automatic theorem prover.
The user can choose certain strategies such as setting searchning depth for the automated theorem prover, but has no control during proving,
The user can choose certain strategies such as setting searching depth for the automated theorem prover, but has no control during proving,
except interrupting it.
In the interactive mode, the process is similar, except that the conjecture along with the graph is limited into those that can be
translated into Coq, and the proof must be done by the user in Coq.
Expand All @@ -159,10 +165,10 @@ A few results of the GTPs are:
:filter: key == 'boutry16'

Tarski's axioms, which are axioms for Euclidean geometry,
is formulated in first-order logic, are formalized in Coq, which 'paves the way for the use of algebraic automated
deduction methods in synthetic geometry within the Coq proof assistant.
is formulated in first-order logic, are formalized in Coq, which "paves the way for the use of algebraic automated
deduction methods in synthetic geometry within the Coq proof assistant".

Usability Evaluation of Interactive Theorem provers
Usability Evaluation of Interactive Theorem Provers
=========================================================
.. container:: bib-item

Expand All @@ -188,7 +194,7 @@ Usability Evaluation of Interactive Theorem provers
The detailed tree-structured proof in KeY is both an advantage and a
disadvantage, since the user can go into details as much as she wants to, but at the same time
it gives too much information that the user does not care about.
However KeY users oftenly have to interact with
However KeY users often have to interact with
low-level logic formulas rather than doing proof on the notation level, and it is common for them to perform repeated low-level interactions.
Isabelle, on the other hand, produces a more intuitive proof.
It also has tools that helps automation such as automated counter example finding. One of the down side of Isabelle is that, finding the right tactic
Expand Down