matita/dist/BUGS \
matita/dist/ChangeLog \
matita/dist/COPYING \
- matita/dist/INSTALL \
- matita/dist/README \
Makefile \
Makefile.defs.in \
$(NULL)
+0.5.6 - 1/12/2008 - bugfix release
+ * more abstract disambiguation algorithm, simpler instantiation
+ to a different CIC/refiner
+ * natural deduction support improved in the first order case
+ * natural deduction lem rule does now support lemmas
+ with (up to) 3 premises (multicut rule, displayed as
+ a collapsed tree)
+
0.5.5 - 17/11/2008 - bugfix release with students in mind
* by ... we proved fixed to use only the specified lemmas but
using full unification inside auto.
+++ /dev/null
-
-Tiny Matita logoMatita Home
-
- Chapter 2. Installation
-Prev Next
-
-━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
-
-Chapter 2. Installation
-
-Table of Contents
-
-Installing from sources
-
- Getting the source code
- Requirements
- (optional) MySQL setup
- Compiling and installing
-
-Configuring Matita
-
-Installing from sources
-
-Currently, the only intended way to install Matita is starting from its source
-code.
-
-Getting the source code
-
-You can get the Matita source code in two ways:
-
- 1. go to the download page and get the latest released source tarball;
-
- 2. get the development sources from our SVN repository. You will need the
- components/ and matita/ directories from the trunk/helm/software/
- directory, plus the configure and Makefile* stuff from the same directory.
-
- In this case you will need to run autoconf before proceding with the
- building instructions below.
-
-Requirements
-
-In order to build Matita from sources you will need some tools and libraries.
-They are listed below.
-
-Note for Debian (and derivatives) users
-
-If you are running a Debian GNU/Linux distribution, or any of its derivative
-like Ubuntu, you can use APT to install all the required tools and libraries
-since they are all part of the Debian archive.
-
-apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev
-liblablgtkmathview-ocaml-dev liblablgtksourceview-ocaml-dev
-libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev
-ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5
-
-An official debian package is going to be added to the archive too.
-
-Required tools and libraries
-
-OCaml
-
- the Objective Caml compiler, version 3.09 or above
-
-Findlib
-
- OCaml package manager, version 1.1.1 or above
-
-OCaml Expat
-
- OCaml bindings for the expat library
-
-GMetaDOM
-
- OCaml bindings for the Gdome 2 library
-
-OCaml HTTP
-
- OCaml library to write HTTP daemons (and clients)
-
-LablGTK
-
- OCaml bindings for the GTK+ library , version 2.6.0 or above
-
-GtkMathView , LablGtkMathView
-
- GTK+ widget to render MathML documents and its OCaml bindings
-
-GtkSourceView , LablGtkSourceView
-
- extension for the GTK+ text widget (adding the typical features of source
- code editors) and its OCaml bindings
-
-MySQL , OCaml MySQL
-
- SQL database and OCaml bindings for its client-side library
-
- The SQL database itself is not strictly needed to run Matita, but the
- client libraries are.
-
-Sqlite , OCaml Sqlite3
-
- Sqlite database and OCaml bindings
-
-Ocamlnet
-
- collection of OCaml libraries to deal with application-level Internet
- protocols and conventions
-
-ulex
-
- Unicode lexer generator for OCaml
-
-CamlZip
-
- OCaml library to access .gz files
-
-(optional) MySQL setup
-
-To fully exploit Matita indexing and search capabilities on a huge metadata set
-you may need a working MySQL database. Detalied instructions on how to do it
-can be found in the MySQL documentation. Here you can find a quick howto.
-
-In order to create a database you need administrator permissions on your MySQL
-installation, usually the root account has them. Once you have the permissions,
-a new database can be created executing mysqladmin create matita (matita is the
-default database name, you can change it using the db.user key of the
-configuration file).
-
-Then you need to grant the necessary access permissions to the database user of
-Matita, typing echo "grant all privileges on matita.* to helm;" | mysql matita
-should do the trick (helm is the default user name used by Matita to access the
-database, you can change it using the db.user key of the configuration file).
-
-Note
-
-This way you create a database named matita on which anyone claiming to be the
-helm user can do everything (like adding dummy data or destroying the contained
-one). It is strongly suggested to apply more fine grained permissions, how to
-do it is out of the scope of this manual.
-
-Compiling and installing
-
-Once you get the source code the installations steps should be quite familiar.
-
-First of all you need to configure the build process executing ./configure.
-This will check that all needed tools and library are installed and prepare the
-sources for compilation and installation.
-
-Quite a few (optional) arguments may be passed to the configure command line to
-change build time parameters. They are listed below, together with their
-default values:
-
-configure command line arguments
-
---with-runtime-dir=dir
-
- (Default: /usr/local/matita) Runtime base directory where all Matita stuff
- (executables, configuration files, standard library, ...) will be installed
-
---with-dbhost=host
-
- (Default: localhost) Default SQL server hostname. Will be used while
- building the standard library during the installation and to create the
- default Matita configuration. May be changed later in configuration file.
-
---enable-debug
-
- (Default: disabled) Enable debugging code. Not for the casual user.
-
-Then you will manage the build and install process using make as usual. Below
-are reported the targets you have to invoke in sequence to build and install:
-
-make targets
-
-world
-
- builds components needed by Matita and Matita itself (in bytecode or native
- code depending on the availability of the OCaml native code compiler)
-
-install
-
- installs Matita related tools, standard library and the needed runtime
- stuff in the proper places on the filesystem.
-
- As a part of the installation process the Matita standard library will be
- compiled, thus testing that the just built matitac compiler works properly.
-
- For this step you will need a working SQL database (for indexing the
- standard library while you are compiling it). See Database setup for
- instructions on how to set it up.
-
-━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
-
-Prev Next
-Matita vs Coq Home Configuring Matita
-
%.gz: %
gzip -c $< > $@
-dist_pre: INSTALL README
-INSTALL: $(MANUAL_DIR)/txt-stamp
- cp $(MANUAL_DIR)/sec_install.txt $@
-$(MANUAL_DIR)/txt-stamp:
- $(MAKE) -C $(MANUAL_DIR) txt-stamp
-
+dist_pre:
+++ /dev/null
-
-MATITA
-------
-
-Matita is a new document-centric interactive theorem prover that integrates
-several Mathematical Knowledge Management tools and techniques.
-
-Matita is traditional. Its logical foundation is the Calculus of (Co)Inductive
-Constructions (CIC). It can re-use mathematical concepts produced by other
-proof assistants like Coq and encoded in an XML encoding of CIC. The
-interaction paradigm of Matita is familiar, being inspired by CtCoq and Proof
-General. Its proof language is procedural in the same spirit of LCF.
-
-Matita is innovative:
-
-- the user interface sports high quality bidimensional rendering of proofs and
- formulae transformed on-the-fly to MathML markup, on which direct
- manipulation of the underlying CIC terms is still possible;
-
-- the knowledge base is distributed: every authored concepts can be published
- becoming part of the Matita library which can be browsed as an hypertext
- (locally or on the World Wide Web) and searched by means of content-based
- queries;
-
-- the tactical language, part of the proof language, has step-by-step
- semantics, enabling inspection and replaying of deeply structured proof
- scripts.
-
-More information are available on the Matita web site:
-
- http://matita.cs.unibo.it/
-
-
-INSTALLATION
-------------
-
-See the file INSTALL for building and installation instructions.
-
-
-BUGS
-----
-
-Bugs reporting is handled using the Bugzilla bug tracker available at:
-
- http://bugs.mowgli.cs.unibo.it/
-
-
-LICENSE
--------
-
-Matita and its documentation are free software.
-See the file COPYING for copying conditions.
-
Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
per rappresentare l'albero di prova del lemma che si sta riutilizzando.
-Per motivi che saranno più chiari una volta studiate logiche del primo ordine
-o di ordine superiore, i lemmi che si intende riutilizzare è bene
-che siano dimostrati astratti sugli atomi, ovvero per ogni
-atomo `A`...`Z` che compare nella formula, è bene aggiungere
-una quantificazione all'inizio della formula stessa (es. `∀A:CProp.`)
-e iniziare la dimostrazione con il comando `assume`. In tale
-modo il lemma EM può essere utilizzato sia per dimostrare
-`A ∨ ¬A` sia `B ∨ ¬B` sia `(A∨C) ∨ ¬(A∨C)` ...
+Per motivi che saranno più chiari una volta studiate logiche del
+primo ordine o di ordine superiore, i lemmi che si intende
+riutilizzare è bene che siano dimostrati astratti sugli atomi.
+Ovvero per ogni atomo `A`...`Z` che compare nella formula,
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`.
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
DOCEND*)
* I nomi delle ipotesi, quando argomenti di
una regola, vengono scritti tra `[` e `]`.
+Le regole di deduzione naturale
+===============================
+
+Per digitare le regole di deduzione naturale
+è possibile utilizzare la palette che compare
+sulla sinistra dopo aver premuto `F2`.
+
+L'albero si descrive partendo dalla radice. Le regole
+con premesse multiple sono seguite da `[`, `|` e `]`.
+Ad esempio:
+
+ apply rule (∧_i (A∨B) ⊥);
+ [ …continua qui il sottoalbero per (A∨B)
+ | …continua qui il sottoalbero per ⊥
+ ]
+
+Le regole vengono applicate alle loro premesse, ovvero
+gli argomenti delle regole sono le formule che normalmente
+scrivete sopra la linea che rappresenta l'applicazione della
+regola stessa. Ad esempio:
+
+ aply rule (∨_e (A∨B) [h1] C [h2] C);
+ [ …prova di (A∨B)
+ | …prova di C sotto l'ipotesi A (di nome h1)
+ | …prova di C sotto l'ipotesi B (di nome h2)
+ ]
+
+Le regole che hanno una sola premessa non vengono seguite
+da parentesi quadre.
+
+L'albero di deduzione
+=====================
+
+Per visualizzare l'albero man mano che viene costruito
+dai comandi impartiti al sistema, premere `F3` e poi
+premere sul bottome home (in genere contraddistinto da
+una icona rappresentate una casa).
+
+Si suggerisce di marcare tale finestra come `always on top`
+utilizzando il menu a tendina che nella maggior parte degli
+ambienti grafici si apre cliccando nel suo angolo in
+alto a sinistra.
+
+Applicazioni di regole errate vengono contrassegnate con
+il colore rosso.
+
+Usare i lemmi dimostrati in precedenza
+======================================
+
+Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
+riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
+
+La "regola" `lem` prende come argomenti:
+
+- Il numero delle ipotesi del lemma che si vuole utilizzare, nel
+ caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
+
+- Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
+
+- Infine, le formule che devono essere scritte come premesse per la
+ "regola".
+
+Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
+`lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
+`lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
+far seguire le parentesi quadre come spiegato in precedenza.
+
+Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
+per rappresentare l'albero di prova del lemma che si sta riutilizzando.
+
+Per motivi che saranno più chiari una volta studiate logiche del
+primo ordine o di ordine superiore, i lemmi che si intende
+riutilizzare è bene che siano dimostrati astratti sugli atomi.
+Ovvero per ogni atomo `A`...`Z` che compare nella formula,
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`.
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
DOCEND*)
axiom S : sort →sort → CProp.
(* assumiamo il terzo escluso *)
-axiom EM : ∀A:CProp.A ∨ ¬A.
+theorem EM: ∀A:CProp. A ∨ ¬ A.
+assume A: CProp.
+apply rule (prove (A ∨ ¬A));
+apply rule (RAA [H] (⊥)).
+apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ apply rule (discharge [H]).
+ | apply rule (⊥_e (⊥));
+ apply rule (¬_e (¬¬A) (¬A));
+ [ apply rule (¬_i [K] (⊥)).
+ apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ apply rule (discharge [H]).
+ | apply rule (∨_i_r (¬A)).
+ apply rule (discharge [K]).
+ ]
+ | apply rule (¬_i [K] (⊥)).
+ apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ apply rule (discharge [H]).
+ | apply rule (∨_i_l (A)).
+ apply rule (discharge [K]).
+ ]
+ ]
+ ]
+qed.
(* intuizionista *)
lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
projects / helm.git / commitdiff