‹header›

‹date/time›

Click to edit Master text styles

Second level

Third level

Fourth level

Fifth level

‹footer›

‹#›

No domain specific knowledge

Say something about derivation trees.

Say something about the structural formulas

Logics are large:

Proof checker must be small.

Uses: Logical framework

Shipment of proofs

Means formalization of proofs

Shipment of proofs

Means formalization of proofs

Shipment of proofs

Means formalization of proofs

Shipment of proofs

Means formalization of proofs

Shipment of proofs

Means formalization of proofs

No domain specific knowledge

Say something about derivation trees.

Say something about the structural formulas

Say : Substitution, weakening and
contraction are implicit.

Ask Frank about what he means with logic
specific theorem provers can be used