forked from FormalizedFormalLogic/Foundation
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLogic.lean
69 lines (52 loc) · 1.92 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
import Logic.Vorspiel.Vorspiel
import Logic.Vorspiel.Order
import Logic.Vorspiel.Meta
import Logic.Logic.LogicSymbol
import Logic.Logic.Semantics
import Logic.Logic.System
import Logic.Logic.HilbertStyle
-- AutoProver
import Logic.AutoProver.Litform
import Logic.AutoProver.Prover
-- Propositional
import Logic.Propositional.Basic.Formula
import Logic.Propositional.Basic.Calculus
import Logic.Propositional.Basic.Semantics
import Logic.Propositional.Basic.Completeness
import Logic.Propositional.Basic
-- 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.Class.Init
import Logic.FirstOrder.Class.Class
import Logic.FirstOrder.Order.Le
import Logic.FirstOrder.Arith.Hierarchy
import Logic.FirstOrder.Arith.StrictHierarchy
import Logic.FirstOrder.Arith.Theory
import Logic.FirstOrder.Arith.Model
import Logic.FirstOrder.Arith.Nonstandard
import Logic.FirstOrder.Arith.PAminus
import Logic.FirstOrder.Incompleteness.FirstIncompleteness
import Logic.FirstOrder.Incompleteness.SelfReference
-- Modal Logic
import Logic.Modal.Normal