Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Raphaël Cauderlier
math_transfer
Commits
6ea52d66
Commit
6ea52d66
authored
Apr 09, 2017
by
Raphael Cauderlier
Browse files
Rename directories
parent
0d3d413c
Changes
39
Hide whitespace changes
Inline
Side-by-side
README.org
View file @
6ea52d66
...
...
@@ -29,16 +29,13 @@ As common formalism in the first step, we use the Dedukti logical
framework\Cite{Dedukti} for which translators from a large variety of
proof systems have been developed.
MathTransfer is composed of a core aiming at solving the second step
and an interoperability library built on top of the core and
consisting in arithmetic and algebraic results imported from various
proof assistants.
MathTransfer is a library aiming at solving the second step. An
example of the use of the library to achieve interoperability is also
provided in the [[./example][example]] directory.
The core of the MathTransfer library consists in formal proofs of
transfer theorems for a variety of mathematical structures coming from
arithmetic and algebra. It is written in FoCaLiZe\Cite{focalize}, a
language that eases the definition of mathematical structures and the
automation of proofs and for which a translator to Dedukti exists.
MathTransfer is written in FoCaLiZe\Cite{focalize}, a language that
eases the definition of mathematical structures and the automation of
proofs and for which a translator to Dedukti exists.
* Installation
...
...
@@ -46,8 +43,6 @@ automation of proofs and for which a translator to Dedukti exists.
The following tools are required to compile the MathTransfer library:
For the core of the library:
- FoCaLiZe version 0.9.2
FoCaLiZe features Dedukti export since version 0.9.2
...
...
@@ -60,8 +55,16 @@ For the core of the library:
- Zenon Modulo version 0.4.3
For the interoperability library, the following extra tools are
required to import logical developments from other proof systems:
- Dktactics
Dktactics is a tactic language for Dedukti
- Dktransfer
Dktransfer is a transfer tactic for Dedukti
Moreover, for the interoperability example, the following extra tools
are required to import logical developments from other proof systems:
- Coq version 8.4pl6
...
...
@@ -113,21 +116,18 @@ To build the library, type the following commands:
$ make
#+END_SRC
* Detailed Content of the MathTransfer library
** Core
The
core of the
MathTransfer library, located in the [[./core][
core
]] directory
The MathTransfer library, located in the [[./core][
lib
]] directory
defines arithmetic and algebraic structures and the morphisms between
such structures but does not contain any interesting properties of
these structures. For example, the structure of natural numbers with
addition is defined in the file [[./
core
/arith/naturals.fcl][
core
/arith/naturals.fcl]] but it does
addition is defined in the file [[./
lib
/arith/naturals.fcl][
lib
/arith/naturals.fcl]] but it does
not contain proofs for the associativity and commutativity of addition
because these properties are not helpful for proving transfer
theorems. It does however contain the theorem statements and proofs
that these properties can be transferred between isomorphic models of
the natural numbers. They can be imported from any arithmetic library so
they are proved in the interoperability library.
the natural numbers. They can be imported from any arithmetic library.
*** Logic
...
...
@@ -137,13 +137,13 @@ seen as an extension of multi-sorted first-order logic.
*** Arithmetic
The directory [[./
core
/arith][
core
/arith]] contains the definitions of arithmetical
The directory [[./
lib
/arith][
lib
/arith]] contains the definitions of arithmetical
structures, that is mathematical structures about natural numbers and
integers.
**** Natural numbers
The file [[./
core
/arith/naturals.fcl][
core
/arith/naturals.fcl]] defines the following species
The file [[./
lib
/arith/naturals.fcl][
lib
/arith/naturals.fcl]] defines the following species
representing mathematical structures built from natural numbers with
various operations and relations:
...
...
@@ -221,7 +221,8 @@ integers.
**** TODO Integers
*** TODO Algebra
* The Interoperability Example
* TODO Related work
...
...
cor
e/Makefile
→
exampl
e/Makefile
View file @
6ea52d66
File moved
interop
/arith/.gitignore
→
example
/arith/.gitignore
View file @
6ea52d66
File moved
interop
/arith/CoqNaturals.v
→
example
/arith/CoqNaturals.v
View file @
6ea52d66
File moved
interop
/arith/Makefile
→
example
/arith/Makefile
View file @
6ea52d66
File moved
interop
/arith/natural_coq.fcl
→
example
/arith/natural_coq.fcl
View file @
6ea52d66
File moved
interop
/arith/natural_full.fcl
→
example
/arith/natural_full.fcl
View file @
6ea52d66
File moved
interop
/arith/natural_hol.fcl
→
example
/arith/natural_hol.fcl
View file @
6ea52d66
File moved
interop
/arith/natural_instantiation.fcl
→
example
/arith/natural_instantiation.fcl
View file @
6ea52d66
File moved
interop
/arith/natural_zenon.fcl
→
example
/arith/natural_zenon.fcl
View file @
6ea52d66
File moved
interop
/arith/update-thm-numbers.el
→
example
/arith/update-thm-numbers.el
View file @
6ea52d66
File moved
interop
/logic/.gitignore
→
example
/logic/.gitignore
View file @
6ea52d66
File moved
interop
/logic/Coq.dk
→
example
/logic/Coq.dk
View file @
6ea52d66
File moved
interop
/logic/Makefile
→
example
/logic/Makefile
View file @
6ea52d66
File moved
interop
/logic/hol_to_coq.dk
→
example
/logic/hol_to_coq.dk
View file @
6ea52d66
File moved
interop
/logic/holtypes.v
→
example
/logic/holtypes.v
View file @
6ea52d66
File moved
core
/.gitignore
→
lib
/.gitignore
View file @
6ea52d66
File moved
interop
/Makefile
→
lib
/Makefile
View file @
6ea52d66
File moved
core
/arith/.gitignore
→
lib
/arith/.gitignore
View file @
6ea52d66
File moved
core
/arith/Makefile
→
lib
/arith/Makefile
View file @
6ea52d66
File moved
Prev
1
2
Next
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment