Commit b30e62f1 authored by Florian Rabe's avatar Florian Rabe

no message

parent ca62044e
......@@ -93,12 +93,18 @@ define temp2
server on 8080
log+ server
log+ debug
//log+ object-checker
log+ object-checker
//log+ object-simplifier
//log+ structure-simplifier
//log+ structure-checker
//log+ object-parser
build MMT/urtheories mmt-omdoc module-expressions.mmt
mathpath archive ../LFX
mathpath archive ../../MitM
//log+ backend
extension info.kwarc.mmt.lf.induction.InductiveTypes
mathpath archive ../../Test/General
//build Test/General mmt-omdoc structures.mmt
build MMT/examples mmt-omdoc inductive.mmt
end
define MMTTest
......@@ -109,7 +115,7 @@ define MMTTest
//log+ structure-checker
//log+ structure-simplifier
//log+ object-parser
log+ object-checker
//log+ object-checker
//log+ object-simplifier
//build MMT/examples mmt-omdoc
mathpath archive ../../Test
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Counter" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#388.15.0:484.18.0"/></metadata><constant name="counter">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#419.16.2:435.16.18"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#428.16.11:430.16.13"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="0"/></om:OMOBJ></definition>
</constant><constant name="add">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#439.17.2:482.17.45"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#444.17.7:453.17.16"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS><om:OMS base="http://cds.omdoc.org/urtheories" module="CF" name="None"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#450.17.13:453.17.16"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#457.17.20:481.17.44"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><om:OMV name="n"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#458.17.21:458.17.21"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#461.17.24:481.17.44"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="CF" name="assign"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Counter" name="counter"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#461.17.24:467.17.30"/></metadata></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#471.17.34:481.17.44"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="plus"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Counter" name="counter"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#471.17.34:477.17.40"/></metadata></om:OMS><om:OMV name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#481.17.44:481.17.44"/></metadata></om:OMV>
</om:OMA>
</om:OMA>
</om:OMBIND></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="LFI" base="http://cds.omdoc.org/examples"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:154.7.0"/></metadata><import from="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#110.5.2:124.5.16"/></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="LFI" base="http://cds.omdoc.org/examples"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:155.7.0"/></metadata><import from="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#110.5.2:124.5.16"/></metadata></import><ruleconstant name="[scala://induction.lf.mmt.kwarc.info?InductiveTypes]"><type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="scala://induction.lf.mmt.kwarc.info" module="InductiveTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#133.6.7:152.6.26"/></metadata></om:OMS></om:OMOBJ></type></ruleconstant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Monoid" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?FOLPatterns"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#154.10.0:201.12.0"/></metadata><derived feature="instance" name="comp" base="http://cds.omdoc.org/examples"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#191.11.6:199.11.14"/></metadata>
<om:OMS base="http://cds.omdoc.org/examples" module="FOLPatterns/fun"></om:OMS>
<om:OMLIT type="http://cds.omdoc.org/urtheories?NatSymbols?NAT" value="2"/>
</om:OMA></type></derived></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Program" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#491.20.0:659.29.0"/></metadata><constant name="main">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#522.21.2:536.21.16"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="CF" name="None"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#529.21.9:535.21.15"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="ProgLang" name="print"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="1"/>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/base-arith.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/base-arith.mmt#0.0.0:1192.32.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Binary]" target="http://cds.omdoc.org/examples?Binary"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/base-arith.mmt#67.3.0:79.3.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/hott.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/hott.mmt#0.0.0:7781.155.0"/></metadata><mref name="[http://cds.omdoc.org/examples?HOTT]" target="http://cds.omdoc.org/examples?HOTT"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/hott.mmt#427.7.0:437.7.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/inductive.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#0.0.0:244.15.0"/></metadata><mref name="[http://cds.omdoc.org/examples?LFI]" target="http://cds.omdoc.org/examples?LFI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:103.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatExample]" target="http://cds.omdoc.org/examples?NatExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#157.9.0:173.9.16"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/inductive.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#0.0.0:263.18.0"/></metadata><mref name="[http://cds.omdoc.org/examples?LFI]" target="http://cds.omdoc.org/examples?LFI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:103.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatExample]" target="http://cds.omdoc.org/examples?NatExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#158.9.0:174.9.16"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/int.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#0.0.0:680.20.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Int]" target="http://cds.omdoc.org/examples?Int"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#42.2.0:51.2.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?IntRules]" target="http://cds.omdoc.org/examples?IntRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#270.10.0:284.10.14"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/literals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#0.0.0:1695.49.0"/></metadata><mref name="[http://cds.omdoc.org/examples?NatLiterals]" target="http://cds.omdoc.org/examples?NatLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#80.4.0:97.4.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?IntLiterals]" target="http://cds.omdoc.org/examples?IntLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#315.13.0:332.13.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Vectors]" target="http://cds.omdoc.org/examples?Vectors"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#584.20.0:597.20.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/fol.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#0.0.0:1072.34.0"/></metadata><mref name="[http://cds.omdoc.org/examples?FOL]" target="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#135.4.0:144.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLNatDed]" target="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#319.11.0:334.11.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLEQ]" target="http://cds.omdoc.org/examples?FOLEQ"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#640.21.0:651.21.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLEQNatDed]" target="http://cds.omdoc.org/examples?FOLEQNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#758.26.0:775.26.17"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/pl.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#0.0.0:2897.85.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#42.2.0:137.3.89"/></metadata>Intuitionistic propositional logic with natural deduction rules and a few example proofs</opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#140.5.0:195.6.48"/></metadata>We start with the syntax of propositional logic.</opaque><mref name="[http://cds.omdoc.org/examples?PL]" target="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#198.8.0:206.8.8"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1233.38.0:1271.38.38"/></metadata>Now we describe the proof theory.</opaque><mref name="[http://cds.omdoc.org/examples?PLNatDed]" target="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1290.40.0:1304.40.14"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/module_expressions.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#0.0.0:917.23.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Algebra]" target="http://cds.omdoc.org/examples?Algebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#43.2.0:56.2.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/nat.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#0.0.0:3499.96.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Bool]" target="http://cds.omdoc.org/examples?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#42.2.0:52.2.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Logic]" target="http://cds.omdoc.org/examples?Logic"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#145.8.0:156.8.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Nat]" target="http://cds.omdoc.org/examples?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#291.14.0:300.14.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatRules]" target="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#709.28.0:723.28.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatMinus]" target="http://cds.omdoc.org/examples?NatMinus"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#2519.77.0:2533.77.14"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#0.0.0:2981.104.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?Syntax]" target="http://cds.omdoc.org/examples/programs?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#51.2.0:63.2.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?Test]" target="http://cds.omdoc.org/examples/programs?Test"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1181.39.0:1191.39.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?Machine]" target="http://cds.omdoc.org/examples/programs?Machine"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1342.49.0:1355.49.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?OperationalSemantics]" target="http://cds.omdoc.org/examples/programs?OperationalSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1682.68.0:1708.68.26"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/programming/semantics.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/semantics.mmt#0.0.0:1350.38.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?OperationalSemantics]" target="http://cds.omdoc.org/examples/programs?OperationalSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/semantics.mmt#51.2.0:77.2.26"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/set.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#0.0.0:3778.66.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Sets]" target="http://cds.omdoc.org/examples?Sets"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#164.5.0:174.5.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/shallow_polymorphism.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#0.0.0:945.25.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Equality]" target="http://cds.omdoc.org/examples?Equality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#99.3.0:113.3.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Lists]" target="http://cds.omdoc.org/examples?Lists"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#586.16.1:597.16.12"/></metadata></mref></omdoc>
\ No newline at end of file
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#0.0.0:7781.166.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#260.6.0:372.6.112"/></metadata>This file contains a definition of first-order logic in MMT as used in the MMT tutorial given at CICM 2016.</opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#376.9.0:451.9.75"/></metadata>A namespace declaration defines the root URI of the following content.</opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#504.12.0:601.12.97"/></metadata>A theory defines a language. It may optionally use a meta-theory, which is given by its URI.</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?FOL]" target="http://cds.omdoc.org/examples/tutorial?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#603.13.0:612.13.9"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#4895.98.0:5059.100.0"/></metadata>Now we define the proof theory of LF using natural deduction proof rules.
It is practical to do this in a separate theory that includes the syntax above.</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?NatDed]" target="http://cds.omdoc.org/examples/tutorial?NatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#5069.101.0:5081.101.12"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#7509.160.0:7693.161.81"/></metadata>The rules declared so far only yield intuitionistic first-order logic. To get to classical logic,
we can use the modular approach and extend NatDed by the law of excluded middle:</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?ClassicalSFOL]" target="http://cds.omdoc.org/examples/tutorial?ClassicalSFOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#7695.162.0:7714.162.19"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/tutorial/3-literalsrules.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#0.0.0:2934.61.0"/></metadata><mref name="[http://cds.omdoc.org/examples/tutorial?Nat]" target="http://cds.omdoc.org/examples/tutorial?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#107.4.0:116.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?NatAsMonoid]" target="http://cds.omdoc.org/examples/tutorial?NatAsMonoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#2763.55.0:2778.55.15"/></metadata></mref></omdoc>
\ No newline at end of file
document http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Types
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Logic
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Equality
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?STT
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Eta
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Extensionality
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?List
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?ListMonad
Declares http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus
document http://docs.omdoc.org/examples/IJCAR2018_example.omdoc
Declares http://docs.omdoc.org/examples/IJCAR2018_example.omdoc http://cds.omdoc.org/examples/ijcar?Nat
Declares http://docs.omdoc.org/examples/IJCAR2018_example.omdoc http://cds.omdoc.org/examples/ijcar?Bool
Declares http://docs.omdoc.org/examples/IJCAR2018_example.omdoc http://cds.omdoc.org/examples/ijcar?DHOL
Declares http://docs.omdoc.org/examples/IJCAR2018_example.omdoc http://cds.omdoc.org/examples/ijcar?Double
document http://docs.omdoc.org/examples/arithmetic_rules.omdoc
Declares http://docs.omdoc.org/examples/arithmetic_rules.omdoc http://cds.omdoc.org/examples?Numbers
Declares http://docs.omdoc.org/examples/arithmetic_rules.omdoc http://cds.omdoc.org/examples?Rules
Declares http://docs.omdoc.org/examples/arithmetic_rules.omdoc http://cds.omdoc.org/examples?Sums
document http://docs.omdoc.org/examples/base-arith.omdoc
Declares http://docs.omdoc.org/examples/base-arith.omdoc http://cds.omdoc.org/examples?Binary
document http://docs.omdoc.org/examples/hott.omdoc
Declares http://docs.omdoc.org/examples/hott.omdoc http://cds.omdoc.org/examples?HOTT
theory http://cds.omdoc.org/examples?LFI
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/mmt?Errors
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?ModExp
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/mmt?mmt
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?Typed
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?TypedConstants
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?KindedConstants
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?TermsTypesKinds
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?LFRules
Includes http://cds.omdoc.org/examples?LFI http://cds.omdoc.org/urtheories?LF
theory http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus
HasMeta http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?STT
Includes http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad
document http://docs.omdoc.org/examples/instances.omdoc
document http://docs.omdoc.org/examples/int.omdoc
Declares http://docs.omdoc.org/examples/int.omdoc http://cds.omdoc.org/examples?Int
Declares http://docs.omdoc.org/examples/int.omdoc http://cds.omdoc.org/examples?IntRules
document http://docs.omdoc.org/examples/literals.omdoc
Declares http://docs.omdoc.org/examples/literals.omdoc http://cds.omdoc.org/examples?NatLiterals
Declares http://docs.omdoc.org/examples/literals.omdoc http://cds.omdoc.org/examples?IntLiterals
Declares http://docs.omdoc.org/examples/literals.omdoc http://cds.omdoc.org/examples?Vectors
document http://docs.omdoc.org/examples/logic
Declares http://docs.omdoc.org/examples/logic http://docs.omdoc.org/examples/logic/opaque_-1393076152
Declares http://docs.omdoc.org/examples/logic http://docs.omdoc.org/examples/logic/fol.omdoc
Declares http://docs.omdoc.org/examples/logic http://docs.omdoc.org/examples/logic/pl.omdoc
Declares http://docs.omdoc.org/examples/logic http://docs.omdoc.org/examples/logic/prover.omdoc
document http://docs.omdoc.org/examples/logic/fol.omdoc
Declares http://docs.omdoc.org/examples/logic/fol.omdoc http://cds.omdoc.org/examples?FOL
Declares http://docs.omdoc.org/examples/logic/fol.omdoc http://cds.omdoc.org/examples?FOLNatDed
Declares http://docs.omdoc.org/examples/logic/fol.omdoc http://cds.omdoc.org/examples?FOLEQ
Declares http://docs.omdoc.org/examples/logic/fol.omdoc http://cds.omdoc.org/examples?FOLEQNatDed
document http://docs.omdoc.org/examples/logic/prover.omdoc
Declares http://docs.omdoc.org/examples/logic/prover.omdoc http://cds.omdoc.org/examples?ProverTest
Declares http://docs.omdoc.org/examples/logic/prover.omdoc http://cds.omdoc.org/examples?PLProofs
Declares http://docs.omdoc.org/examples/logic/prover.omdoc http://cds.omdoc.org/examples?FOLProofs
document http://docs.omdoc.org/examples/module_expressions.omdoc
Declares http://docs.omdoc.org/examples/module_expressions.omdoc http://cds.omdoc.org/examples?Algebra
document http://docs.omdoc.org/examples/nat.omdoc
Declares http://docs.omdoc.org/examples/nat.omdoc http://cds.omdoc.org/examples?Bool
Declares http://docs.omdoc.org/examples/nat.omdoc http://cds.omdoc.org/examples?Logic
Declares http://docs.omdoc.org/examples/nat.omdoc http://cds.omdoc.org/examples?Nat
Declares http://docs.omdoc.org/examples/nat.omdoc http://cds.omdoc.org/examples?NatRules
Declares http://docs.omdoc.org/examples/nat.omdoc http://cds.omdoc.org/examples?NatMinus
document http://docs.omdoc.org/examples/patterns.omdoc
Declares http://docs.omdoc.org/examples/patterns.omdoc http://cds.omdoc.org/examples?FOLPatterns
Declares http://docs.omdoc.org/examples/patterns.omdoc http://cds.omdoc.org/examples?Monoid
document http://docs.omdoc.org/examples/program.omdoc
Declares http://docs.omdoc.org/examples/program.omdoc http://cds.omdoc.org/examples?ProgLang
Declares http://docs.omdoc.org/examples/program.omdoc http://cds.omdoc.org/examples?Counter
Declares http://docs.omdoc.org/examples/program.omdoc http://cds.omdoc.org/examples?Program
document http://docs.omdoc.org/examples/programming
Declares http://docs.omdoc.org/examples/programming http://docs.omdoc.org/examples/programming/machine.omdoc
Declares http://docs.omdoc.org/examples/programming http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc
Declares http://docs.omdoc.org/examples/programming http://docs.omdoc.org/examples/programming/semantics.omdoc
Declares http://docs.omdoc.org/examples/programming http://docs.omdoc.org/examples/programming/syntax.omdoc
document http://docs.omdoc.org/examples/programming/machine.omdoc
Declares http://docs.omdoc.org/examples/programming/machine.omdoc http://cds.omdoc.org/examples/programs?Machine
document http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc
Declares http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc http://cds.omdoc.org/examples/programs?Syntax
Declares http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc http://cds.omdoc.org/examples/programs?Test
Declares http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc http://cds.omdoc.org/examples/programs?Machine
Declares http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc http://cds.omdoc.org/examples/programs?OperationalSemantics
document http://docs.omdoc.org/examples/programming/semantics.omdoc
Declares http://docs.omdoc.org/examples/programming/semantics.omdoc http://cds.omdoc.org/examples/programs?OperationalSemantics
document http://docs.omdoc.org/examples/programming/syntax.omdoc
Declares http://docs.omdoc.org/examples/programming/syntax.omdoc http://cds.omdoc.org/examples/programs?Syntax
Declares http://docs.omdoc.org/examples/programming/syntax.omdoc http://cds.omdoc.org/examples/programs?Test
document http://docs.omdoc.org/examples/quantities.omdoc
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?Quantities
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?Dimensions
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?Prefixes
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?Units
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?DerivedUnits
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?CookingUnit
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?TimeUnits
Declares http://docs.omdoc.org/examples/quantities.omdoc http://cds.omdoc.org/physics?TemperatureUnits
document http://docs.omdoc.org/examples/real.omdoc
Declares http://docs.omdoc.org/examples/real.omdoc http://docs.omdoc.org/examples/real.omdoc/opaque_-1846079735
Declares http://docs.omdoc.org/examples/real.omdoc http://cds.omdoc.org/examples?Real
document http://docs.omdoc.org/examples/sequences.omdoc
Declares http://docs.omdoc.org/examples/sequences.omdoc http://cds.omdoc.org/examples?FlexaryConnectives
Declares http://docs.omdoc.org/examples/sequences.omdoc http://cds.omdoc.org/examples?FlexaryQuantifiers
document http://docs.omdoc.org/examples/set.omdoc
Declares http://docs.omdoc.org/examples/set.omdoc http://cds.omdoc.org/examples?Sets
document http://docs.omdoc.org/examples/shallow_polymorphism.omdoc
Declares http://docs.omdoc.org/examples/shallow_polymorphism.omdoc http://cds.omdoc.org/examples?Equality
Declares http://docs.omdoc.org/examples/shallow_polymorphism.omdoc http://cds.omdoc.org/examples?Lists
document http://docs.omdoc.org/examples/sigma.omdoc
Declares http://docs.omdoc.org/examples/sigma.omdoc http://cds.omdoc.org/examples?DepSumChurch
document http://docs.omdoc.org/examples/tutorial
Declares http://docs.omdoc.org/examples/tutorial http://docs.omdoc.org/examples/tutorial/0-Tutorial.omdoc
Declares http://docs.omdoc.org/examples/tutorial http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc
Declares http://docs.omdoc.org/examples/tutorial http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc
Declares http://docs.omdoc.org/examples/tutorial http://docs.omdoc.org/examples/tutorial/3-literalsrules.omdoc
document http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc/opaque_-1193362204
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc/opaque_-707977531
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc/opaque_1439403531
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://cds.omdoc.org/examples/tutorial?FOL
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc/opaque_-1158276115
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://cds.omdoc.org/examples/tutorial?NatDed
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc/opaque_1701138502
Declares http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc http://cds.omdoc.org/examples/tutorial?ClassicalSFOL
document http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc/opaque_1073579727
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?Semigroup
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?Monoid
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?PreOrder
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?MonoidAsPreorder
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?Abelian
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?Group
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?AbelianGroup
Declares http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc http://cds.omdoc.org/examples/tutorial?Ring
document http://docs.omdoc.org/examples/tutorial/3-literalsrules.omdoc
Declares http://docs.omdoc.org/examples/tutorial/3-literalsrules.omdoc http://cds.omdoc.org/examples/tutorial?Nat
Declares http://docs.omdoc.org/examples/tutorial/3-literalsrules.omdoc http://cds.omdoc.org/examples/tutorial?NatAsMonoid
......@@ -4,11 +4,11 @@ import rules scala://induction.lf.mmt.kwarc.info❚
theory LFI =
include ur:?LF
rule rules?InductiveRule
rule rules?InductiveTypes

theory NatExample : ?LFI =
inductive nat ❘=
inductive nat()❘=
n: type
z: n
s: n ⟶ n
......
......@@ -18,7 +18,7 @@ theory Quantities : ur:?LF =
comm : {d:dim,e:dim} d*e=e*d❙
mult_scalar_right : {d} d*scalar = d ❘role Simplify❙
mult_scalar_left : {d} scalar*d = d ❘role Simplify❙
mult_inv_right : {d:dim} d*d⁻ = scalar ❘role Simplify❙
mult_inv_right : {d:dim} d*d⁻ = scalar ❘role Simplify❙
mult_inv_left : {d:dim} d⁻*d = scalar ❘role Simplify❙
inv_mult : {d:dim,e:dim} (d*e)⁻ = d⁻*e⁻ ❘role Simplify❙
inv_inv : {d} d⁻⁻ = d ❘role Simplify❙
......
......@@ -25,7 +25,7 @@ theory Monoid : ?NatDed =
unit_axiom : ⊢ ∀[x] x ∘ e = x❘ @_description the axiom of the neutral element ❙
theory PreOrder : ?NatDed =
o : sort ❙
order : tm o ⟶ tm o ⟶ prop ❘ # 1 ≤ 2 prec 50 ❙
......
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