Commit b36fb641 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Typos

parent a85dc907
...@@ -130,7 +130,7 @@ by logical connectives and quantifiers. ...@@ -130,7 +130,7 @@ by logical connectives and quantifiers.
An atom is a predicate symbol applied to terms respecting the arity of An atom is a predicate symbol applied to terms respecting the arity of
the predicate symbol. Predicate symbols and their arities are defined the predicate symbol. Predicate symbols and their arities are defined
similarly to function symbols. A predicate symbol is a Dedukti term of similarly to function symbols. A predicate symbol is a Dedukti term of
type =fol.predicate=. An artity is is associated to each predicate type =fol.predicate=. An artity is associated to each predicate
symbol by the function symbol by the function
- =fol.pred_arity : fol.predicate -> fol.types= - =fol.pred_arity : fol.predicate -> fol.types=
...@@ -220,7 +220,7 @@ definable so Deduction Modulo first-order theories can be defined. ...@@ -220,7 +220,7 @@ definable so Deduction Modulo first-order theories can be defined.
** Equality ** Equality
We treat equality as a first-order theory defined in the file We treat equality as a first-order theory defined in the file
[[./fol/eq.dl][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by [[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
a sort: a sort:
- =eq.Eq : fol.type -> fol.predicate= - =eq.Eq : fol.type -> fol.predicate=
...@@ -251,14 +251,14 @@ facts: ...@@ -251,14 +251,14 @@ facts:
The Dedukti theory presented in [[* Multi-sorted first-order logic in Dedukti][the previous section]] is sound in the The Dedukti theory presented in [[* Multi-sorted first-order logic in Dedukti][the previous section]] is sound in the
following sense: following sense:
- Convergence: The rewrite system that defines it is both confluent - Convergence: The rewrite system that defines it is both confluent
and terminating and terminating.
- Subject-reduction: Typing is preserved by reduction according to - Subject-reduction: Typing is preserved by reduction according to
this rewrite-system this rewrite-system.
- Decidability of type-checking: The type-checking problem for terms - Decidability of type-checking: The type-checking problem for terms
in this Dedukti theory is decidable and the Dedukti type checker is in this Dedukti theory is decidable and the Dedukti type checker is
a decision procedure for it. a decision procedure for it.
- Consistency: a closed term of type =fol.proof fol.false= can only be - Consistency: a closed term of type =fol.proof fol.false= can only be
obtained by encoding an inconsistent first-order theory obtained by encoding an inconsistent first-order theory.
Thanks to these good properties, a term of type =fol.proof A= can be Thanks to these good properties, a term of type =fol.proof A= can be
considered as a proof witnessing the truth of the proposition =A=. We considered as a proof witnessing the truth of the proposition =A=. We
...@@ -277,10 +277,10 @@ The first bad system is a dependently-typed tactic language. It is ...@@ -277,10 +277,10 @@ The first bad system is a dependently-typed tactic language. It is
very similar to the typed tactic languages of Lean and [[http://plv.mpi-sws.org/mtac/][Mtac]] but it is very similar to the typed tactic languages of Lean and [[http://plv.mpi-sws.org/mtac/][Mtac]] but it is
simpler for the following reasons: simpler for the following reasons:
- It deals with first-order logic instead of the full calculus of - It deals with first-order logic instead of the full calculus of
inductive constructions inductive constructions.
- In Dedukti it is not necessary to encode pattern matching and - In Dedukti it is not necessary to encode pattern matching and
recursion directly in the tactic language because the user can recursion directly in the tactic language because the user can
already use rewriting for these tasks already use rewriting for these tasks.
- We have chosen to keep a shallow encoding of terms and formulae so - We have chosen to keep a shallow encoding of terms and formulae so
some features such as testing whether a term is a variable are some features such as testing whether a term is a variable are
omitted. omitted.
...@@ -296,7 +296,7 @@ to handle failure and backtracking. ...@@ -296,7 +296,7 @@ to handle failure and backtracking.
- =tac.bind : A : fol.prop -> B : fol.prop -> tac.tactic A -> (fol.proof A -> tac.tactic B) -> tac.tactic B= - =tac.bind : A : fol.prop -> B : fol.prop -> tac.tactic A -> (fol.proof A -> tac.tactic B) -> tac.tactic B=
If =A= is a formula, =tac.tactic A= is the Dedukti type of the tactics If =A= is a formula, =tac.tactic A= is the Dedukti type of the tactics
attempting to prove =A=. It forms a monad whise return and bind attempting to prove =A=. It forms a monad whose return and bind
operations are =tac.ret= and =tac.bind= respectively. operations are =tac.ret= and =tac.bind= respectively.
When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =tac.run=: When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =tac.run=:
...@@ -359,7 +359,7 @@ The certificate language is described in file [[./meta/cert.dk][meta/cert.dk]]. ...@@ -359,7 +359,7 @@ The certificate language is described in file [[./meta/cert.dk][meta/cert.dk]].
** Contexts and certificate evaluation ** Contexts and certificate evaluation
=certificate= is the Dedukti type of certificates. Contrary to =cert.certificate= is the Dedukti type of certificates. Contrary to
tactics, the type of a certificate does not indicate which formula it tactics, the type of a certificate does not indicate which formula it
is supposed to prove and the same certificate can in fact prove is supposed to prove and the same certificate can in fact prove
several formulae. several formulae.
...@@ -546,8 +546,8 @@ The certificate =cert.apply A B a c= proves =B a= if =c= proves ...@@ -546,8 +546,8 @@ The certificate =cert.apply A B a c= proves =B a= if =c= proves
*** Reasoning on the goal *** Reasoning on the goal
The following certificates each prove the current goal if it has a The following certificates are used to reason on the current goal,
particular shape: each proves the current goal if it has a particular shape:
- =cert.trivial : cert.certificate= - =cert.trivial : cert.certificate=
- =cert.split : cert.certificate -> cert.certificate -> cert.certificate= - =cert.split : cert.certificate -> cert.certificate -> cert.certificate=
- =cert.left : cert.certificate -> cert.certificate= - =cert.left : cert.certificate -> cert.certificate=
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol")) (setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;) ;)
(; This is a Meta Dedukti port Mtac with the following simpifications: (; This is a Meta Dedukti port of Mtac with the following simpifications:
- works on first-order logic instead of CIC - works on first-order logic instead of CIC
This implies a bit of duplication between terms and proofs. This implies a bit of duplication between terms and proofs.
- nu and abs are replaced by the less powerful but simpler to implement intro - nu and abs are replaced by the less powerful but simpler to implement intro
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment