4.5 Reasoning

Page 31 of 800

Search internet

Logiweb is developed for formal reasoning. It is easy to reason about Logiweb programs because they are just extended lambda terms (extended in that they may include true, If-then-else, and quote).

Furthermore, Logiweb has a long list of features which makes it suited for writing proof checkers:

• Logiweb has the quote feature which allows to convert a term into a representation of that term. The quote feature corresponds to Gödel brackets.
• Logiweb has an author defined source syntax: The author of a Logiweb page can define his or her own syntax for entering terms. As an example, the author may choose to use all x : y to denote universal quantification in the source syntax. This makes it easier to formulate axioms, lemmas, and proofs.
• Logiweb has an author defined rendering syntax. When the author runs a Logiweb source text (an lgs text) through the Logiweb compiler (lgc), the compiler generates a rendering of the page which is suited for publication on the Internet. As an example of use, the author of a page may choose to use as the rendering of all x : y.
• Logiweb allows to build on top of the work of others: A Logiweb page can reference other Logiweb pages. Doing so, the syntax, rendering, axioms, lemmas, proofs, programs, and so on from the referenced pages become available on the referencing page. As an example, a proof on a Logiweb page may build upon lemmas published by others.

Page 31 of 800

Search logiweb.eu