contour.git
5 years agoAdded example files, removed debugging info. master
ethereal [Fri, 18 Apr 2014 05:33:45 +0000 (23:33 -0600)]
Added example files, removed debugging info.

5 years agoCode cleanups.
ethereal [Fri, 18 Apr 2014 05:25:59 +0000 (23:25 -0600)]
Code cleanups.

5 years agoFixed bug where both invertible/non-invertible rules applicable.
ethereal [Fri, 18 Apr 2014 04:52:10 +0000 (22:52 -0600)]
Fixed bug where both invertible/non-invertible rules applicable.

5 years agoBugfix for issue introduced by earlier code cleanup.
ethereal [Fri, 18 Apr 2014 04:16:16 +0000 (22:16 -0600)]
Bugfix for issue introduced by earlier code cleanup.

However, ((A|B)>(A|B)) is not recognized as a theorem. This should be fixed.

5 years agoRemoved more memory leaks.
ethereal [Fri, 18 Apr 2014 04:10:06 +0000 (22:10 -0600)]
Removed more memory leaks.

Valgrind output is clean now.

5 years agoCleaned up codebase significantly.
ethereal [Fri, 18 Apr 2014 03:53:37 +0000 (21:53 -0600)]
Cleaned up codebase significantly.

5 years agoAdded support for invertible rules, fixed some memory leaks.
ethereal [Fri, 18 Apr 2014 03:26:38 +0000 (21:26 -0600)]
Added support for invertible rules, fixed some memory leaks.

5 years agoFix some small bugs.
ethereal [Sat, 12 Apr 2014 18:40:09 +0000 (12:40 -0600)]
Fix some small bugs.

5 years agoAdded LaTeX output formatting.
ethereal [Sat, 12 Apr 2014 02:05:48 +0000 (20:05 -0600)]
Added LaTeX output formatting.

5 years agoAdded nicer proof formatting.
ethereal [Fri, 11 Apr 2014 20:27:35 +0000 (14:27 -0600)]
Added nicer proof formatting.

Next up: bussproofs.sty-style proof output.

5 years agoFixed missing node type.
ethereal [Fri, 11 Apr 2014 20:20:23 +0000 (14:20 -0600)]
Fixed missing node type.

5 years agoSeveral fixes. Still a bug to find...
ethereal [Fri, 11 Apr 2014 20:16:42 +0000 (14:16 -0600)]
Several fixes. Still a bug to find...

5 years agoSimple sentences are being proved correctly.
ethereal [Fri, 11 Apr 2014 19:20:35 +0000 (13:20 -0600)]
Simple sentences are being proved correctly.

5 years agoImplemented brute-force DFS proof-search, untested.
ethereal [Fri, 11 Apr 2014 17:58:28 +0000 (11:58 -0600)]
Implemented brute-force DFS proof-search, untested.

There are likely bugs. Time to find them!

5 years ago(Hopefully) implemented all rules.
ethereal [Fri, 11 Apr 2014 17:43:24 +0000 (11:43 -0600)]
(Hopefully) implemented all rules.

Now for the prover.

5 years agoChanged negation to \implies absurdity, added disjunction rules.
ethereal [Thu, 10 Apr 2014 06:31:38 +0000 (00:31 -0600)]
Changed negation to \implies absurdity, added disjunction rules.

5 years agoInitial rule-application structure implemented.
ethereal [Mon, 31 Mar 2014 07:25:44 +0000 (01:25 -0600)]
Initial rule-application structure implemented.

Next up: a significant amount more rule implementations . . .

5 years agoFixed small bug in parser. Copy-paste = bad.
ethereal [Mon, 31 Mar 2014 05:35:08 +0000 (23:35 -0600)]
Fixed small bug in parser. Copy-paste = bad.

5 years agoInitial parser/tree representation finished.
ethereal [Mon, 31 Mar 2014 05:23:55 +0000 (23:23 -0600)]
Initial parser/tree representation finished.