Commit b119c8c77913894eb0f10b708929d53f4f1ed1c2 - Maxixe

Update the README and the Design document. Chris Pressey 6 years ago

2 changed file(s) with 17 addition(s) and 11 deletion(s). Raw diff Collapse all Expand all

-4

README.md less more

30	30
31	31	For examples of proofs witten in Maxixe, see [doc/Examples.md](doc/Examples.md).
32	32
33		The reference implementation of Maxixe, called `maxixe`, is written in Python 2.7.
34		Simply add the `bin` directory of this repository to your executable search path
	33	The reference implementation of Maxixe, called `maxixe`, is written in Python,
	34	and runs under (at least) Python 2.7.12 and Python 3.5.2. To use `maxixe`,
	35	simply add the `bin` directory of this repository to your executable search path
35	36	and run it on a text file containing your proof, like
36	37
37	38	maxixe my_proof.maxixe

49	50	Note that since Maxixe requires that you supply all the axioms and rules of
50	51	inference used in a proof, it is entirely possible to give it an inconsistent
51	52	system of logic in which anything can be proved — but that's not quite the
52		same thing as what I'm talking about. Such a proof is still valid relative
53		to its axioms and rules of inference.
	53	same thing as what I'm talking about. Such a proof is still "valid", relative
	54	to logic that it is using.
54	55
55	56	But on that note, I am also not prepared to claim that all of the rules of
56	57	inference I've used in the example proofs Maxixe are consistent (or otherwise

+12

-7

doc/Design.md less more

16	16	stated.
17	17
18	18	* Generality: the proof language itself should make as few assumptions about
19		the object language as possible. In particular, it shouldn't "know logic".
	19	the object language as possible. It shouldn't be tied to any particular system
	20	of logic — as far as possible, it should be purely a [proof calculus][].
20	21
21	22	* Predicate Logic: on the other hand, the proof language should, when given
22	23	the rules of predicate logic, be powerful enough to allow one to check proofs
23		using predicate logic.
	24	using predicate logic (a.k.a. first-order logic).
24	25
25	26	* Correctness: the proof-checking capability of the language must not
26	27	claim that an incorrect proof is correct for the given rules. It would also

50	51
51	52	* Generality: instead of coding the rules for Existential Instantiation (etc) in
52	53	the proof language, we have coded constraints on hypotheses and conclusions which
53		allow rules like EI to be written.
	54	allow rules like EI to be written. It's basically a [natural deduction][]-like system
	55	in which propositional logic, predicate logic, and other logics (ones that
	56	don't rely too heavily on side conditions for their rules) can be captured.
54	57
55		* Predicate Logic: see the Generality point above. It's probably close, but I wouldn't
56		put money on it quite yet.
	58	* Predicate Logic: see the Generality point above. I believe the examples show
	59	that a significant portion, if not all, of first-order logic, can be coded in Maxixe.
57	60
58		* Correctness: see the Disclaimer in the README. It's probably close, but I wouldn't
59		put money on it quite yet.
	61	* Correctness: see the Disclaimer in the README. It's probably very close, but I
	62	wouldn't put money on it quite yet. Bugs are always possible.
60	63
61	64	Related Work
62	65	------------

95	98	[The Incredible Proof Machine]: http://incredible.pm/
96	99	[Post canonical systems]: https://en.wikipedia.org/wiki/Post_canonical_system
97	100	[MetaMath]: http://us.metamath.org/
	101	[proof calculus]: https://en.wikipedia.org/wiki/Proof_calculus
	102	[natural deduction]: https://en.wikipedia.org/wiki/Natural_deduction