Check-in [adaef9d668]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Comment:Fixed a minor typo.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
User & Date: andy 2015-04-20 09:52:40
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). check-in: 1252a63f55 user: andy tags: bc-subst
Fixed a minor typo. Leaf check-in: adaef9d668 user: andy tags: trunk
Final draft of report. (Unless I think of something else to add...) check-in: 04f1cd0696 user: andy tags: trunk
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

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