Commit 89fd147aff46c5c767d045e9dfc7437719d9355a - Eqthy

+6

-5

README.md less more

62	62	detrimental to simplicity, and vice versa.
63	63
64	64	It has been implemented in Python 3 in about 720 lines of code; the core
65		verifier module is less than 150 lines of code. For more details, see
66		the [Implementations](#implementations) section below.
	65	(term manipulation and verifier modules) is about 340 lines of code. For
	66	more details, see the [Implementations](#implementations) section below.
67	67
68	68	It is also possible for a human to write Eqthy documents by hand, and
69	69	to read them, without much specialized knowledge. The base logic

108	108
109	109	### Desired Examples
110	110
111		* [Interior algebra](https://en.wikipedia.org/wiki/Interior_algebra) (corresponding to the modal logic S4)
112	111	* [Relation algebra](https://en.wikipedia.org/wiki/Relation_algebra)
113		* Johnson's 1892 axiom system given in Meredith and Prior's 1967 paper [Equational Logic](https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093893457)
114		* The theorem of ring theory given in [Equational Logic, Spring 2017](https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf) by McNulty (but it's a bit of a monster all right)
	112	* Johnson's 1892 axiom system given in Meredith and Prior's 1967 paper
	113	[Equational Logic](https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093893457)
	114	* The theorem of ring theory given in [Equational Logic, Spring 2017](https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf)
	115	by George McNulty (but it's a bit of a monster all right)
115	116
116	117	### Aspirational Items
117	118

+4

-2

eg/algebra-of-sets.eqthy.md less more

12	12	I'm told they are subtlely different, but aren't their axioms basically the same? The difference
13	13	may be too subtle to matter for our purposes here.
14	14
15		Anyway, I'm writing this so I can have an algebra of sets to base some further set-based
16		definitions on, in lieu of having an actual set theory.
	15	Anyway, I'm writing this so I can have an theory of sets to base further definitions on.
	16	I don't have a "proper" set theory (defining ZFC in equational logic is rather out
	17	of the question), and it would seem awkward to base some of those further definitions
	18	on Boolean algebra, so this algebra of sets will need to suffice for a basis.
17	19
18	20	Commutative properties:
19	21

+1

-0

eg/set-difference.eqthy.md less more

23	23	axiom (#inter-id) inter(A, u) = A
24	24	axiom (#union-comp) union(A, comp(A)) = u
25	25	axiom (#inter-comp) inter(A, comp(A)) = e
	26
26	27	axiom (#union-de-morg) comp(inter(A, B)) = union(comp(A), comp(B))
27	28	axiom (#inter-de-morg) comp(union(A, B)) = inter(comp(A), comp(B))
28	29

+3

-3

src/eqthy/main.py less more

4	4	from argparse import ArgumentParser
5	5	import codecs
6	6	import sys
7		from typing import List, Dict
	7	from typing import List
8	8
9		from eqthy.objects import Theorem
	9	from eqthy.objects import Context
10	10	from eqthy.parser import Parser
11	11	from eqthy.verifier import Verifier
12	12

53	53
54	54	options = argparser.parse_args(args)
55	55
	56	context: Context = {}
56	57	try:
57		context: Dict[str, Theorem] = {}
58	58	for filename in options.input_files:
59	59	with codecs.open(filename, 'r', encoding='UTF-8') as f:
60	60	text = f.read()

+4

-1

src/eqthy/objects.py less more

3	3
4	4	"""Objects in the Eqthy document structure."""
5	5	from dataclasses import dataclass
6		from typing import List, Union
	6	from typing import List, Dict, Union
7	7	from .terms import Eqn, Term, Variable
8	8
9	9

60	60	class Document:
61	61	axioms: List[Axiom]
62	62	theorems: List[Theorem]
	63
	64
	65	Context = Dict[str, Theorem]

+4

-4

src/eqthy/verifier.py less more

4	4	from typing import Dict, Union, Any
5	5
6	6	from eqthy.objects import (
7		Document, Theorem, Step,
	7	Context, Document, Theorem, Step,
8	8	Reflexivity, Substitution, Congruence, Reference
9	9	)
10	10	from eqthy.terms import (

18	18
19	19
20	20	class Verifier:
21		def __init__(self, document: Document, verbose: bool = True, context: Union[Dict[str, Theorem], None] = None):
	21	def __init__(self, document: Document, verbose: bool = True, context: Union[Context, None] = None):
22	22	self.axioms = document.axioms
23	23	self.theorems = document.theorems
24	24	self.verbose = verbose
25		self.context: Dict[str, Theorem] = context or {}
	25	self.context: Context = context or {}
26	26	self.rules: Dict[str, RewriteRule] = {}
27	27
28	28	for axiom in self.axioms:

37	37	self.rules[name + '_1'] = RewriteRule(pattern=lhs, substitution=rhs)
38	38	self.rules[name + '_2'] = RewriteRule(pattern=rhs, substitution=lhs)
39	39
40		def verify(self) -> Dict[str, Theorem]:
	40	def verify(self) -> Context:
41	41	for theorem in self.theorems:
42	42	self.verify_theorem(theorem)
43	43	self.register(theorem.name, theorem.eqn.lhs, theorem.eqn.rhs)