93db8d02b5
Implement tightness check
2020-05-29 14:57:00 +02:00
491a255811
Require supertight programs for backward proof
2020-05-28 05:03:56 +02:00
0578e99dc2
Finish basic simplifications
2020-05-22 18:14:56 +02:00
3b3f9017ba
Determine variable IDs correctly
2020-05-22 02:42:38 +02:00
81ddfd450a
Use custom foliage flavor
...
With this patch, properties specific to variable, function, and
predicate declarations are directly stored within those objects rather
than external maps that need to be queried via traits. This greatly
simplifies many parts of the logic.
This is made possible by implementing a custom foliage flavor, which
makes it possible to swap the built-in declaration types for extended
versions of those types that fulfill certain requirements.
2020-05-22 02:25:00 +02:00
34b8dce9be
Ignore built-in predicates in completion
2020-05-19 12:54:51 +02:00
4de4cc21da
Fix gross bug in translation of division
2020-05-18 05:21:27 +02:00
84031c483b
Revert logic for building completed definitions
2020-05-13 03:27:47 +02:00
d35d0d1d98
Use statement kind over section kind
2020-05-13 03:17:33 +02:00
0dbf30bb1b
Work in progress
2020-05-13 02:24:13 +02:00
4d00fbeb97
Minor formatting
2020-05-13 01:40:44 +02:00
674cee0e87
Remove obsolete to-do note
2020-05-11 04:00:51 +02:00
ab7c6d1828
Rename ScopedFormula to OpenFormula
2020-05-11 03:58:30 +02:00
2c660ff902
Remove unused code
2020-05-11 03:39:09 +02:00
c075f99093
Remove unused code
2020-05-11 02:43:42 +02:00
753cc3e5a8
Improve output
2020-05-07 17:19:42 +02:00
b55bc82b1d
Add option for proof direction
2020-05-07 02:53:48 +02:00
e118442e16
Work in progress
2020-05-05 19:40:57 +02:00
07322f041c
Use foliage traits
2020-04-17 04:10:23 +02:00
e6cf79ad1e
Remove unneeded indirection
2020-04-17 03:37:53 +02:00
eb60bd7520
Refactor variable declaration stack usage
2020-04-17 03:28:18 +02:00
84bec338ae
Use foliage’s built-in variable declaration stack
2020-04-17 01:45:41 +02:00
becd8d4c19
Upgrade to foliage 0.2 development version
2020-04-17 00:09:44 +02:00
f83695b5dc
Move closure functions to utils module
2020-02-09 10:26:24 +07:00
c3860c1bf1
Check variable declaration stack before using it
2020-02-09 10:22:08 +07:00
f6f423e307
Add axioms for order of symbolic constants
2020-02-05 20:19:22 +01:00
b6ecf37211
Add option for input constants
2020-02-05 19:40:21 +01:00
844f81f5b5
Count program and integer variable IDs separately
2020-02-05 18:50:48 +01:00
26c1bde49b
Move variable declaration stack from foliage crate
2020-02-05 02:30:17 +01:00
2bc084d799
Finish implementing TPTP output
2020-02-05 02:14:47 +01:00
caab0a618e
Add option for input predicates
2020-02-05 01:10:33 +01:00
ce19860325
Make all terms compatible in TPTP
2020-02-04 23:33:59 +01:00
d7f04da0bd
Restructure project
2020-02-04 16:53:52 +01:00
f5b84eaf63
Restructure project
2020-02-04 16:48:33 +01:00
3dbe11be61
Restructure project
2020-02-04 16:45:13 +01:00
87a3517bfb
Restructure project
2020-02-04 16:42:50 +01:00
a9ef9d2496
Minor refactoring
2020-02-04 15:15:11 +01:00
2ad5396488
Add option for human-readable output
2020-02-04 00:27:04 +01:00
072fa34e69
Refactoring to support TPTP output
2020-02-03 02:57:45 +01:00
0714bed2cc
Start supporting TPTP output
2020-02-02 20:27:30 +01:00
5ad14f8deb
Add option for specifying input files
2020-02-02 19:20:16 +01:00
e122532fcb
Implement completion
2020-02-02 17:57:27 +01:00
28a804409c
Support choice rules with single atom in head
2020-02-02 03:56:51 +01:00
23641987bc
Persist declarations between rules
2020-02-02 02:53:04 +01:00
99345bc0ac
Finish implementing definitions
2020-02-02 02:32:32 +01:00
86c8391278
Refactoring
2020-02-01 21:59:36 +01:00
24980d5a8d
Refactoring to drop Context type
2020-02-01 19:20:46 +01:00
66902c1888
Rename module for determining head type
2020-02-01 17:20:43 +01:00
142531d334
Determine head type of input rules
2020-02-01 17:13:43 +01:00
aaea04d51b
Work in progress
2020-02-01 16:05:06 +01:00
