10.1 Introduction

Prev Up Next Page 368 of 800 Search internet

Logiweb pages can be used for stating definitions, programs, theories, lemmas, proofs, and other entities which can be processed by computers. Some examples follow:

A definition

The combinations page gives an example of programming in Logiweb by defining the binomial coefficient. You will learn how to produce a similar page in Tutorial T02.

A proof

The multzero page proves all x : 0 * x = 0. The Logiweb compiler automatically verifies proofs like the one on the multzero page whenever it translates a page. You will learn how to produce a similar page in Tutorial T03.

A proof checker

The check page implements a proof checker which is based on the 'Logiweb sequent calculus'. The proof checker allows users to define axioms, inference rules, and theories, and to state lemmas and proofs. The proof checker checks each proof against the theory in which the associated lemma is stated.

An axiomatic theory

The Peano page defines classical propositional calculus (Prop), classical first order logic (FOL), and Peano arithmetic (PA). Furthermore, the Peano page defines a tactic which allows users to use deduction in their proofs. The Peano page contains a proof of x + y = y + x which illustrates how to use the facilities. If you want to write Logiweb proofs, do not miss reading the sources of the proofs (available by clicking 'Source' on the Peano page. Reading the sources is like learning html by reading html sources. The Peano page references both the base and the check page to get access to macro facilities as well as the proof checker. Users who want to define other theories like ZFC may benefit from referencing the base, check, and Peano pages to get access to macros, proof checker, and FOL. Make sure you reference the check page as first reference: that ensures that your page is checked using the proof checker.

A compiler

The lgc page defines the Logiweb compiler.

A testsuite

The test page defines one among the Logiweb regression testsuites.

A base page

The base page defines a lot of elementary constructs.

The base page happens to be a 'Logiweb base page', i.e. a Logiweb page which references no other pages. For that reason, the base page cannot rely on any definitions on any other page. Rather, the base page defines everything bottom up starting from scratch. Here are some examples of what the base page defines:

Prev Up Next Page 368 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05