Check-in [adaef9d668]

Not logged in

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 2015-04-20 09:52:40
Context
2015-04-20
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). check-in: 1252a63f55 user: andy tags: bc-subst
09:52
Fixed a minor typo. Leaf check-in: adaef9d668 user: andy tags: trunk
2015-04-18
21:14
Final draft of report. (Unless I think of something else to add...) check-in: 04f1cd0696 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
Curry-Howard 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 in-progress 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
Curry-Howard 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 in-progress 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.