Patrick Lühne
9b6632cc94
Check that only input predicates are used in assumptions
2020-05-29 17:42:05 +02:00
Patrick Lühne
93db8d02b5
Implement tightness check
2020-05-29 14:57:00 +02:00
Patrick Lühne
b52ca236e2
Handle private predicates in specification
2020-05-28 07:27:29 +02:00
Patrick Lühne
1b827edd45
Clean-up
2020-05-28 05:03:56 +02:00
Patrick Lühne
491a255811
Require supertight programs for backward proof
2020-05-28 05:03:56 +02:00
Patrick Lühne
9b7895a032
Don’t append variable ID if there is only one
2020-05-22 19:43:41 +02:00
Patrick Lühne
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
Patrick Lühne
86d2857494
Start implementation of simplifications
2020-05-19 12:56:46 +02:00
Patrick Lühne
80d39c8c0a
Check that only input/output predicates are used in specification
2020-05-18 02:17:30 +02:00
Patrick Lühne
58d89b4d07
Detect cyclic dependencies when hiding predicates
2020-05-18 01:19:59 +02:00
Patrick Lühne
82422cc28f
Support hiding auxiliary predicates
2020-05-13 08:02:04 +02:00
Patrick Lühne
ab7c6d1828
Rename ScopedFormula to OpenFormula
2020-05-11 03:58:30 +02:00
Patrick Lühne
7c36c4b239
Move closure functions to separate module
2020-05-11 03:41:33 +02:00
Patrick Lühne
84bec338ae
Use foliage’s built-in variable declaration stack
2020-04-17 01:45:41 +02:00
Patrick Lühne
c3860c1bf1
Check variable declaration stack before using it
2020-02-09 10:22:08 +07:00
Patrick Lühne
26c1bde49b
Move variable declaration stack from foliage crate
2020-02-05 02:30:17 +01:00
Patrick Lühne
2bc084d799
Finish implementing TPTP output
2020-02-05 02:14:47 +01:00
Patrick Lühne
ce19860325
Make all terms compatible in TPTP
2020-02-04 23:33:59 +01:00