First draft for interactive theorem provers #14

rinshankaihou · 2019-11-21T05:03:12Z

There are still contents to add, and citation to fix.

cyrus-

The format is not correct -- you need to have bib items with summaries, as in notation.rst. Please correct this and make the other suggested changes for your second draft.

cyrus- · 2019-11-25T23:09:14Z

src/itp.rst

@@ -0,0 +1,139 @@
+.. :Authors: - Cyrus Omar


add your name here

cyrus- · 2019-11-25T23:09:26Z

src/itp.rst

@@ -0,0 +1,139 @@
+.. :Authors: - Cyrus Omar
+
+.. title:: Interactive Theorem Prover


"Prover" -> "Provers"

cyrus- · 2019-11-25T23:11:04Z

src/itp.rst

+  .. bibliography:: itp.bib
+    :filter: key == 'Klein2009'
+
+  Complete formal verification is the only known way to guarantee that a system is free of programming errors. 


This statement is not a summary of the Klein et al 2009 paper. This can be the first sentence of your Overview but this paper should be separately summarized.

I just want this to be an introduction, rather than introducing this paper; maybe I should clarify this more.

cyrus- · 2019-11-25T23:11:30Z

src/itp.rst

+  .. bibliography:: itp.bib
+    :filter: key == '10.1007/BFb0000430'
+
+  while the flaws are counterintuitive enough so that an informal analysis may be too prone to error


again, this is not a summary of the cited paper.

cyrus- · 2019-11-25T23:12:17Z

src/itp.rst

+  while the flaws are counterintuitive enough so that an informal analysis may be too prone to error
+  to be reliable.
+
+An `interactive theorem prover <https://en.wikipedia.org/wiki/Proof_assistant>`_, sometimes refered as proof assistant, is a software that helps 


don't link to Wikipedia

"refered" -> "referred to"

"a software" -> "a programming environment"

cyrus- · 2019-11-25T23:31:40Z

src/itp.rst

+
+Usability Evaluation of Interactive Theorem provers
+=========================================================
+[EVAL] performs usability evaluation using focus groups.


again, bib item

cyrus- · 2019-11-25T23:59:28Z

src/itp.rst

+
+The evaluation involves discussion about two interactive theorem provers, KeY and Isabelle.
+The KeY system is an interactive verification system for programs
+written in Java annotated with the Java Modelling Language. The user interface is tree-structured,


"Modelling" -> "Modeling"

cyrus- · 2019-11-25T23:59:51Z

src/itp.rst

+The KeY system is an interactive verification system for programs
+written in Java annotated with the Java Modelling Language. The user interface is tree-structured,
+each node is an intermediate goal, and the children are derived from applying formulas to their parent node,
+whereas Isabelle only shows the current goal, and by applying tactics (sometimes called methods), which are essentially 


run-on sentence, start a new sentence about Isabelle

cyrus- · 2019-11-26T00:00:21Z

src/itp.rst

+it gives too much information that the user does not care about. 
+However KeY users oftenly have to interact with
+low-level logic formulas rather than doing proof on the notation level, and low-level steps are oftenly repeated by hand. 
+Isabelle, on the other hand, produces intuitive proof.


"produces intuitive proof" -> "produces a more intuitive proof"

cyrus- · 2019-11-26T00:01:10Z

src/index.rst

+  \part{Interactive Theorem Prover}
+
+.. toctree::
+  :caption: Interactive Theorem Prover


this should go in the Live Programming chapter, not in a separate top-level chapter like this

cyrus-

good topic coverage and paper descriptions overall. need a little more work introducing various topics before talking about their results (see comments). second draft grade will be sent by email.

cyrus- · 2019-12-06T22:20:20Z

src/itp.bib

+@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},


22Nd -> 22nd

cyrus- · 2019-12-06T22:20:36Z

src/itp.bib

@@ -0,0 +1,120 @@
+@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},


acronyms in bibtex titles need to be in braces to avoid capitalization changes: {OS}

cyrus- · 2019-12-06T22:21:19Z

src/itp.bib

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


Formal names need to be braced: {Tarski}, {Descartes}, etc.

cyrus- · 2019-12-06T22:21:29Z

src/itp.bib

+}
+
+@inproceedings{lerner15,
+  title={Polymorphic blocks: Formalism-inspired UI for structured connectors},


cyrus- · 2019-12-06T22:21:39Z

src/itp.bib

+}
+
+@inproceedings{aspinall00,
+  title={Proof General: A generic tool for proof development},


{Proof General}

cyrus- · 2019-12-06T22:26:11Z

src/itp.rst

+is completely rigorous, and is oftenly tedious and hard.
+
+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.


use the phrase "trusted computing base (TCB)" here, since that shows up in a lot of papers

cyrus- · 2019-12-06T22:26:32Z

src/itp.rst

+
+
+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


"appropraite" -> "appropriate"

cyrus- · 2019-12-06T22:26:49Z

src/itp.rst

+  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,


"searchning" -> "searching"

cyrus- · 2019-12-06T22:27:04Z

src/itp.rst

+    :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 


didn't conclude the quote here

cyrus- · 2019-12-06T22:27:19Z

src/itp.rst

+  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


"provers" -> "Provers"

cyrus- · 2019-12-06T22:29:54Z

src/itp.rst

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


the next sentence restates this sentence, so just remove this one

cyrus- · 2019-12-06T22:31:10Z

src/itp.rst

+  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


This isn't a general topic, it's a specific system. Maybe call these "Live Interactive Theorem Provers", and add the evaluation paper about KeY and Isabelle in to that section instead of having them separated

cyrus-

thanks! will send final grades by email soon

cyrus- · 2019-12-23T16:31:08Z

src/itp.bib

@@ -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},


"Euclidean" should also be capitalized

rinshankaihou added 3 commits November 20, 2019 00:41

real init

cb607d9

almost

237e7b9

todo fix citation

364a6f9

cyrus- requested changes Nov 26, 2019

View reviewed changes

rinshankaihou added 2 commits December 3, 2019 18:42

basically done; need to check grammer

ef81460

second draft

d713498

cyrus- requested changes Dec 6, 2019

View reviewed changes

cyrus- reviewed Dec 6, 2019

View reviewed changes

final draft

2ef50dd

cyrus- approved these changes Dec 23, 2019

View reviewed changes

Base automatically changed from master to trunk February 14, 2021 02:52

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

First draft for interactive theorem provers #14

First draft for interactive theorem provers #14

rinshankaihou commented Nov 21, 2019

cyrus- left a comment

cyrus- Nov 25, 2019

cyrus- Nov 25, 2019

cyrus- Nov 25, 2019

rinshankaihou Dec 3, 2019

cyrus- Nov 25, 2019

cyrus- Nov 25, 2019

cyrus- Nov 25, 2019

cyrus- Nov 25, 2019

cyrus- Nov 25, 2019

cyrus- Nov 26, 2019

cyrus- Nov 26, 2019

cyrus- left a comment

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- Dec 6, 2019

cyrus- left a comment

cyrus- Dec 23, 2019

		@@ -0,0 +1,139 @@
		.. :Authors: - Cyrus Omar

		.. title:: Interactive Theorem Prover



		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

First draft for interactive theorem provers #14

Are you sure you want to change the base?

First draft for interactive theorem provers #14

Conversation

rinshankaihou commented Nov 21, 2019

cyrus- left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrus- left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrus- left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment