forked from FormalizedFormalLogic/Foundation
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Logic.lean
75 lines (56 loc) · 2.14 KB
/
Logic.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
import Logic.Vorspiel.Vorspiel
import Logic.Vorspiel.Order
import Logic.Vorspiel.Meta
import Logic.Logic.LogicSymbol
import Logic.Logic.Semantics
import Logic.Logic.System
-- AutoProver
import Logic.AutoProver.Litform
import Logic.AutoProver.Prover
-- Propositional
import Logic.Propositional.Classical.Basic.Formula
import Logic.Propositional.Classical.Basic.Calculus
import Logic.Propositional.Classical.Basic.Semantics
import Logic.Propositional.Classical.Basic.Completeness
import Logic.Propositional.Classical.Basic
-- Propositional Intuitionistic
import Logic.Propositional.Intuitionistic
import Logic.Propositional.Translation
-- FirstOrder
import Logic.FirstOrder.Basic.Syntax.Language
import Logic.FirstOrder.Basic.Syntax.Term
import Logic.FirstOrder.Basic.Syntax.Formula
import Logic.FirstOrder.Basic.Syntax.Rew
import Logic.FirstOrder.Basic.Semantics.Semantics
import Logic.FirstOrder.Basic.Semantics.Elementary
import Logic.FirstOrder.Basic.Calculus
import Logic.FirstOrder.Basic.Operator
import Logic.FirstOrder.Basic.Elab
import Logic.FirstOrder.Basic.Eq
import Logic.FirstOrder.Basic.Soundness
import Logic.FirstOrder.Basic
import Logic.FirstOrder.Hauptsatz
import Logic.FirstOrder.Ultraproduct
import Logic.FirstOrder.Computability.Term
import Logic.FirstOrder.Computability.Formula
import Logic.FirstOrder.Computability.Coding
import Logic.FirstOrder.Computability.Calculus
import Logic.FirstOrder.Completeness.Coding
import Logic.FirstOrder.Completeness.SubLanguage
import Logic.FirstOrder.Completeness.SearchTree
import Logic.FirstOrder.Completeness.Completeness
import Logic.FirstOrder.Order.Le
import Logic.FirstOrder.Interpretation
import Logic.FirstOrder.Arith.Basic
import Logic.FirstOrder.Arith.Hierarchy
import Logic.FirstOrder.Arith.StrictHierarchy
import Logic.FirstOrder.Arith.Theory
import Logic.FirstOrder.Arith.Model
import Logic.FirstOrder.Arith.PeanoMinus
import Logic.FirstOrder.Arith.Representation
import Logic.FirstOrder.Arith.Nonstandard
import Logic.FirstOrder.Arith.EA.Basic
import Logic.FirstOrder.Incompleteness.FirstIncompleteness
import Logic.FirstOrder.Incompleteness.SelfReference
-- Modal Logic
import Logic.Modal.Normal