Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
Overview
Comment:  Fixed a minor typo. 

Downloads:  Tarball  ZIP archive  SQL archive 
Timelines:  family  ancestors  descendants  both  trunk 
Files:  files  file ages  folders 
SHA1:  adaef9d6687d28386f6bb138fde8000cc79ecfa8 
User & Date:  andy 20150420 09:52:40 
Context
20150420
 
09:54  Started work on making backchaining of goals a) apply the substitution to the expansion, rather than appending it as a conjunction of unifications, b) return the substitution along with each branch of the expansion, and c), return the name of the branch that was chosen (analogous to the index N parameter in `choice` proofs). checkin: 1252a63f55 user: andy tags: bcsubst  
09:52  Fixed a minor typo. Leaf checkin: adaef9d668 user: andy tags: trunk  
20150418
 
21:14  Final draft of report. (Unless I think of something else to add...) checkin: 04f1cd0696 user: andy tags: trunk  
Changes
Changes to report/arendreport.pdf.
cannot compute difference between binary files
Changes to report/arendreport.tex.
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 
CurryHoward isomorphism; although its proofs are terms, it does not check them
by computing their types, since terms in Arend are untyped. Nonetheless, we
believe that it should be possible to derive a consistent type system from
Arend's reasoning logic, which would support this interpretation.
Proof assistants that present a graphical interface are rare.
While graphical ``wrappers'' exist for some systems (for example,
ProofWeb\link{http://prover.cs.ru.nl/login.php} for Coq),
these were not a part of the design of their underlying
systems. The only proof assistant of which we are aware which makes graphical
interaction as much an integral feature as Arend is HLM
\mcitep{reichelt2010types}. Like Arend, HLM encourages direct manipulation
of inprogress proofs and is explicitly designed with that hope that it will
make building proofs ``fun'', but unlike Arend, it is based on classical, rather than constructive logic, and has a more mathematical, and less
pedagogical, aim.

 
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 
CurryHoward isomorphism; although its proofs are terms, it does not check them
by computing their types, since terms in Arend are untyped. Nonetheless, we
believe that it should be possible to derive a consistent type system from
Arend's reasoning logic, which would support this interpretation.
Proof assistants that present a graphical interface are rare.
While graphical ``wrappers'' exist for some systems (for example,
\link{http://prover.cs.ru.nl/login.php}{ProofWeb} for Coq),
these were not a part of the design of their underlying
systems. The only proof assistant of which we are aware which makes graphical
interaction as much an integral feature as Arend is HLM
\mcitep{reichelt2010types}. Like Arend, HLM encourages direct manipulation
of inprogress proofs and is explicitly designed with that hope that it will
make building proofs ``fun'', but unlike Arend, it is based on classical, rather than constructive logic, and has a more mathematical, and less
pedagogical, aim.
