abdc8c3bcf5b761e9bebf51e6ba2bce659d29512 |
|
08-Apr-2018 |
Eugen Kuksa <kuksa.eugen@gmail.com> |
Reasoning with database (#1836)
* First step towards saving reasoning results in the database.
* Add first steps of SInE premise selection.
* Try again with 'flattenComorphism'.
* Improve SInE implementation.
* Adjust GraphQL resolvers to new action field.
* Fix rebasing mistakes.
* Fix timeLimit.
* moved let variables to where clause with scoped type vars
* Fix errors in reasoning.
* Fix some more errors in SInE.
* fixed typing problems
* Debug Reasoning.
* Fix compile-time errors.
* Mode debugging.
* made coercion type safe
* Remove commented code.
* Re-implement proving for the REST interface.
* Cleanup.
* Fix SInE selection.
* Cleanup.
* Fix SInE.
* Fix provers command.
* Fix column name.
* Remove commented out code.
* Capture consistency checker output.
* Obey Review.
* Obey review.
* Obey Review.
* Refactor buildReasoningCache.
* Add name to LogicTranslation and get rid of compiler warnings.
* Save all sentences in the database instead of only local ones.
* Rename column to make it more compact.
* Add name to LogicInclusion.
* Save used sentences of a proof attempt. |