Commit a7d9a993 authored by Florian Rabe's avatar Florian Rabe

no message

parent 3777800c
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/prover.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#0.0.0:754.33.0"/></metadata><mref name="[http://cds.omdoc.org/examples?ProverTest]" target="http://cds.omdoc.org/examples?ProverTest"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#42.2.0:58.2.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?PLProofs]" target="http://cds.omdoc.org/examples?PLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#293.19.0:307.19.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLProofs]" target="http://cds.omdoc.org/examples?FOLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:516.28.15"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/logic/prover.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#0.0.0:933.40.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><mref name="[http://cds.omdoc.org/examples?ProverTest]" target="http://cds.omdoc.org/examples?ProverTest"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#42.2.0:58.2.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?PLProofs]" target="http://cds.omdoc.org/examples?PLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#295.19.0:309.19.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLProofs]" target="http://cds.omdoc.org/examples?FOLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#670.32.0:685.32.15"/></metadata></mref></omdoc>
\ No newline at end of file
datatypeconstructor http://cds.omdoc.org/examples?Equality?equal
datatypeconstructor http://cds.omdoc.org/examples?Equality?eq
dataconstructor http://cds.omdoc.org/examples?Equality?refl
dataconstructor http://cds.omdoc.org/examples?Equality?cong
dataconstructor http://cds.omdoc.org/examples?Equality?cast
dataconstructor http://cds.omdoc.org/examples?Equality?sym
dataconstructor http://cds.omdoc.org/examples?Equality?trans
theory http://cds.omdoc.org/examples?Equality
HasMeta http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/urtheories?PLF
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?equal
constant http://cds.omdoc.org/examples?Equality?equal
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?eq
constant http://cds.omdoc.org/examples?Equality?eq
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?refl
constant http://cds.omdoc.org/examples?Equality?refl
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?cong
constant http://cds.omdoc.org/examples?Equality?cong
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?cast
constant http://cds.omdoc.org/examples?Equality?cast
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?sym
constant http://cds.omdoc.org/examples?Equality?sym
Declares http://cds.omdoc.org/examples?Equality http://cds.omdoc.org/examples?Equality?trans
constant http://cds.omdoc.org/examples?Equality?trans
dataconstructor http://cds.omdoc.org/examples?FOLProofs?test
dataconstructor http://cds.omdoc.org/examples?FOLProofs?test2
theory http://cds.omdoc.org/examples?FOLProofs
HasMeta http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/examples?PL
Includes http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/examples?FOL
Includes http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/examples?PLNatDed
Includes http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/examples?FOLNatDed
Declares http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/examples?FOLProofs?test
constant http://cds.omdoc.org/examples?FOLProofs?test
Declares http://cds.omdoc.org/examples?FOLProofs http://cds.omdoc.org/examples?FOLProofs?test2
constant http://cds.omdoc.org/examples?FOLProofs?test2
......@@ -15,7 +15,6 @@ dataconstructor http://cds.omdoc.org/examples?PLNatDed?equivEr
dataconstructor http://cds.omdoc.org/examples?PLNatDed?imp2I
dataconstructor http://cds.omdoc.org/examples?PLNatDed?imp2E
dataconstructor http://cds.omdoc.org/examples?PLNatDed?example
dataconstructor http://cds.omdoc.org/examples?PLNatDed?interactive_example
theory http://cds.omdoc.org/examples?PLNatDed
HasMeta http://cds.omdoc.org/examples?PLNatDed http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples?PLNatDed http://cds.omdoc.org/examples?PL
......@@ -53,5 +52,3 @@ Declares http://cds.omdoc.org/examples?PLNatDed http://cds.omdoc.org/examples?PL
constant http://cds.omdoc.org/examples?PLNatDed?imp2E
Declares http://cds.omdoc.org/examples?PLNatDed http://cds.omdoc.org/examples?PLNatDed?example
constant http://cds.omdoc.org/examples?PLNatDed?example
Declares http://cds.omdoc.org/examples?PLNatDed http://cds.omdoc.org/examples?PLNatDed?interactive_example
constant http://cds.omdoc.org/examples?PLNatDed?interactive_example
dataconstructor http://cds.omdoc.org/examples?PLProofs?test2
dataconstructor http://cds.omdoc.org/examples?PLProofs?interactive_example
theory http://cds.omdoc.org/examples?PLProofs
HasMeta http://cds.omdoc.org/examples?PLProofs http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples?PLProofs http://cds.omdoc.org/examples?PL
Includes http://cds.omdoc.org/examples?PLProofs http://cds.omdoc.org/examples?PLNatDed
Includes http://cds.omdoc.org/examples?PLProofs http://cds.omdoc.org/examples?ProofIrrelevance
Declares http://cds.omdoc.org/examples?PLProofs http://cds.omdoc.org/examples?PLProofs?test2
constant http://cds.omdoc.org/examples?PLProofs?test2
Declares http://cds.omdoc.org/examples?PLProofs http://cds.omdoc.org/examples?PLProofs?interactive_example
constant http://cds.omdoc.org/examples?PLProofs?interactive_example
......@@ -3,3 +3,4 @@ Declares http://docs.omdoc.org/examples/logic/pl.omdoc http://docs.omdoc.org/exa
Declares http://docs.omdoc.org/examples/logic/pl.omdoc http://cds.omdoc.org/examples?PL
Declares http://docs.omdoc.org/examples/logic/pl.omdoc http://docs.omdoc.org/examples/logic/pl.omdoc/opaque_380314106
Declares http://docs.omdoc.org/examples/logic/pl.omdoc http://cds.omdoc.org/examples?PLNatDed
Declares http://docs.omdoc.org/examples/logic/pl.omdoc http://cds.omdoc.org/examples?ProofIrrelevance
......@@ -18,7 +18,7 @@ theory PL : http://cds.omdoc.org/urtheories?LF =
/T Given [F:prop], the type $⊦ F$ holds the proofs of $F$.❙
ded : prop ⟶ type ❘ # ⊦ 1 prec -5❘role Judgment❙
## Abbreviations❙
/T The type $contra$ abbreviates the judgment of inconsistency.
......@@ -85,6 +85,11 @@ theory PLNatDed : http://cds.omdoc.org/urtheories?LF =
example : {A} ⊦ A ⇒ (A ∧ A) ❘
= [A]impI [p]andI p p❙
interactive_example : {A} ⊦ A ⇒ (A ∧ A)❘
= ≪{A} ⊦ A⇒A∧A≫ ❙
import rules scala://lf.mmt.kwarc.info❚
theory ProofIrrelevance : http://cds.omdoc.org/urtheories?LF =
include ?PL❙
/T a rule that makes all terms of type ded F equal❙
rule rules?TermIrrelevanceRule ded❙
\ No newline at end of file
......@@ -14,21 +14,27 @@ theory ProverTest : http://cds.omdoc.org/urtheories?LF =
q: d ⟶ d❙
test : a ⟶ a ⟶ d ❘ = [x,y] ≪d ≫❙
test : a ⟶ a ⟶ d ❘ = ≪a ⟶ a ⟶ d ≫❙
theory PLProofs : http://cds.omdoc.org/urtheories?LF =
include ?PLNatDed❙
include ?ProofIrrelevance❙
/T this doesn't work currently
/T Not all of the automated proofs work at the moment.
// test : {a,b} ⊦ (a ∧ b) ⇒ (b ∧ a)❘ = _❙
// test2 : {a,b} ⊦ (a ∨ b) ⇒ (b ∨ a)❘ = _❙
test : {a,b} ⊦ (a ∧ b) ⇒ (b ∧ a)❘ = _❙
test2 : {a,b} ⊦ (a ∨ b) ⇒ (b ∨ a)❘ // = _❙
interactive_example : {A} ⊦ A ⇒ (A ∧ A)❘
= ≪{A:prop}⊦A⇒A∧A≫ ❙
theory FOLProofs : http://cds.omdoc.org/urtheories?LF =
include ?FOLNatDed❙
// test : {f} ⊦ (forall [x] forall [y] f x y) ⇒ (forall [y] forall [x] f x y) ❘= _❙
// test2 : {f} ⊦ (exists [x] exists [y] f x y) ⇒ (exists [y] exists [x] f x y) ❘= _❙
test : {f} ⊦ (forall [x] forall [y] f x y) ⇒ (forall [y] forall [x] f x y) ❘
// = _❘❙
test2 : {f} ⊦ (exists [x] exists [y] f x y) ⇒ (exists [y] exists [x] f x y) ❘
// = _❘❙
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