Back to MathWiki main page

LogiWeb

One would have expected that all of mathematics would have been machine formalized some decades after the invention of the digital computer. But it seems that something has been missing for that to happen. Logiweb (http://logiweb.eu/) was conceived in an attempt to analyse what was missing. And it was designed and implemented 1996-2006 to meet the following objectives: Accumulation of knowledge: Once a machine formalized development was published on Logiweb, the publication should remain accessible in unchanged form forever. This simply mimics what publishing houses and libraries provide for ordinary mathematics. Standing on the shoulders of predecessors: When proving a theorem, users should be able to draw upon theorems proved by others. This simply mimics the way any mathematician works. Notational freedom: Each user should be free to use any notation. That freedom should come without restricting the notational freedom of others. And differences in notation should be no obstacle when using the results of others. Foundational freedom: Each user should be free to choose what mathematical foundation to work upon. Import of results from one foundation to another should be possible (but not neccessarily trivial). Distribution: Access to the work of others should happen transparently via the Internet. Readibility: Users should be able to publish articles on Logiweb which are as readable as any mathematics book one can pick from any library. Accommodation: Users should be able to publish anything from short notes to multi-volume works that span thousands of pages. Scalability: The system should allow an arbitrary number of submissions and should run smoothly up to 10^18 papers. Simplicity: The system should be so simple that its core could be implemented by a single person. And so simple that once it was implemented, a graduate computer science student could re-implement it in one year. Extensibility: Once the core was implemented, users should be able to adapt the system without changing the core and should be able to publish adaptations on Logiweb itself to make the adaptations available to other users. Verification: Logiweb should be able to tell whether or not a publication is correct. In the spirit of accumulation, correctness should be time independent such that a publication which is deemed correct at one time should remain correct forever. Logiweb is a rather simple system which fulfills the objectives above. The talk gives a walk-through of the system. Furthermore, the talk describes how Logiweb can interface to other systems like wiki systems and other proof systems.

talk/demo on Wikicoqweb: Proofs for freshmen with Coqweb

Coqweb is a web interface for Coq, primarily designed for teaching. It allows teachers to propose statements in sufficiently familiar form. Students are invited to prove these statements essentially by clicking. Hints can be given in natural language, in which case the interface checks that the student somehow understands the hints. We present here the main features of Coqweb, and show through examples how it has been used since 2004.

Formal Reasoning with Different Logical Foundations

Mizar

We will present the key aspects of the Mizar technology for formalizing mathematics as well as building and maintaining a database of formalized and semantically linked knowledge - Mizar Mathematical Library. We will focus on the issues relevant to the WWW environment: XML-based presentation, querying with MMLQuery and on-line processing of Mizar documents.

Logosphere

Asynchronous processing of proof documents -- rethinking interactive theorem proving

The classical model of interactive proof-checking is best illustrated by the de-facto standard user-interface, namely Proof General. Here the user operates on a collection of theory files, while editing the body of a single theory works by stepping back and forth in a strictly sequential (synchronous) fashion. I would like to take a fresh look at how proof documents are processed. Both the increased demands of large formalizations should be addressed, as well as multi-processing that has become readily available now. Ultimately, user-interfaces and related prover protocols with the following characteristics should emerge: - Less requirements on the "editor" component, i.e. make it work with simple web interfaces, rather than demanding a "rich client" architecture. - The prover should be able to re-order and re-schedule individual theory and proof transactions according to their inherent dependencies. - The user should be able to edit theory sources very freely, with the system maintaining consistency as expected. Here the inherent structure of a proof language like Isar admits the outline to be checked quickly, while the sub-proofs may be refined later by iterative deepening. - Editing of unfinished, partially broken theories and proofs should be easy (in fact the norm rather than the exception). Thus we hope to increase effectiveness of interactive theorem proving significantly, enabling users to work on much larger formalizations.

Collaborative Editing with PGIP

We will give a fresh view on the display side of the PGIP protocol, which connects interface front-ends (called displays) with the central PGIP middleware (and hence the provers). This stateless display protocol can be conveniently modelled as a REST-style interface with XUpdate messages signalling changes. From there, we discuss possibilities for collaborative editing in this context-- it turns out that collaborative editing is more or less built in, but needs to be restricted to make it useful.

Challenges to a global web-based library of formal mathematics

(Based on discussions with Cezary Kaliszyk and Pierre Corbineau)

I will discuss what I perceive to be the possibilities for developing a "Wiki for Formalized Mathematics" within a joint European ICT project. I see two main motivations for such a system: - Cooperative work on a large repository of formalized mathematics. This is also to solve the problem that "there is not enough mathematics formalized". - Providing high level access to a repository of formal maths. When searching for a mathematical notion, one should also get a comprehensible link to the formalization. This should also help solve the "access problem": what is in the repository? In the talk I will discuss what could be done and what I think should be done. Audience participation during the talk is very much appreciated.

Documenting and Editing Formal Mathematics in Natural Language

- GF: translations between languages (both formal and natural) - GF Resource Grammar Library: high-level programming of grammatically correct translation rules - embedded grammars in JavaScript: automatic generation of multilingual syntax editors from GF grammars - using embedded JavaScript grammars in Wiki pages

Teaching logic using a web interface for Coq

We will present the system ProofWeb, that allows teaching students logic using an interactive web interface to the proof assistant Coq. First we will present a general framework for creating responsive web interfaces to proof assistants, which allows the students to use the system without the need to install anything (not even a browser plug-in). On top of that we will present an extension for teaching, that makes the full power of Coq available to the students, but simultaneously presents the logic problems in a way that is customary in undergraduate logic courses. Both styles of presenting natural deduction proofs (Gentzen-style `tree view' and Fitch-style `box view') are supported. The system allows the teachers to centrally track progress of the students. We will present a database of logic problems, that also holds the students solutions and a parser that indicates whether the students used only the allowed inference rules of the logic.

A prototype system for collaborative proving

We present a framework for the online development of formalized mathematics. This framework allows wiki-style collaboration while providing users with a rendered and browsable version of their work. We describe a prototype for Coq, based on the web interface implemented by Cezary Kaliszyk (which he will present in his talk), and a modified version of the MediaWiki code-base. Then, we will focus on cross-file consistency and dependency issues with concurrent access and write, and finally on requirements for supporting existing proof assistants.

An Implicational Logic for Conjecturing and Distributed Proof Attempts

I will introduce a logic of implication which supports making conjectures as a basic operation. This allows them to be used before they are proved as well as reused in different branches of a proof and in different parts of a theory. This forms a meta-theory for theories which allows distributed proof attempts while maintaining the interdependencies between lemmas. I hope to develop this into a full type theory which gives keeps support for distributed development.

A glimpse of Evgeny Makarov's abstract and modular formalisation of arithmetic in Coq

Evgeny Makarov formalised basic axiomatic arithmetic in Coq. He came up with two sets of Peano-style axioms that characterise respectively natural numbers and integers and differ only in saying whether every number has a predecessor. Then he derived generic lemmas about "plus", "times", "less than" and a setoid equality. New functions can be defined generically using Peano's recursion or by axiomatising their defining properties and providing implementations of these properties for various datatypes (zero-and-successor numbers, binary numbers, etc.). Theorems proved from defining properties hold for every implementation. Automation such as polynomial simplification (the ring tactic) directly hold from the genericity of Barras-Gregoire-Mahboubi implementation. Generic decision of linear arithmetic (and beyond), is work in progress. From the "math wiki" perspective, we wonder whether focusing on a well-delimited mathematical theory such as the one used to formalise arithmetic, or more generally number theory, could provide an interesting first step to make both human beings and the different proof assistants agree on a common high-level domain-specific mathematical vernacular.

Obstacles to a global library of formal mathematics

I will discuss what I perceive to be the main reasons that there is not yet a large scale effort to create a good and comprehensive library of formal mathematics.

Providing mathematical Web services with Symbolic Computation Software Composability Protocol

Modern symbolic computations require infrastructure for parallel algorithms and combining capabilities available in several different systems. Moreover, there are growing numbers of symbolic computation resources, such as databases or specialised software which could be made available as Web services or Grid services accessible over the Internet. The EU Framework VI project "SCIEnce --- Symbolic Computation Infrastructure in Europe" (http://www.symbolic-computation.org/) addresses these needs of the symbolic computation user community. First we designed the Symbolic Computation Software Composibility Protocol (SCSCP) by which a computer algebra system (CAS) may offer services and a client may employ them. We envisage clients for this protocol including: - A Web server which passes on the same services as Web services using SOAP/HTTP protocols to a variety of possible clients; - Grid middleware; - Another instance of the same CAS (in a parallel computing context); - Another CAS running on the same computer system or remotely. All messages in the protocol are represented as OpenMath objects (http://www.openmath.org). In my talk I will give more details about OpenMath and SCSCP, and will demonstrate some examples using SCSCP implementation for the computational algebra system GAP (http://www.gap-system.org).

Back to MathWiki main page

Randy Pollack Last modified: Mon Nov 19 13:49:21 GMT 2007