Commit Graph

29 Commits

Author SHA1 Message Date
Patrick Lühne aec76f39cf
Support integer constant declarations 2019-11-07 03:14:44 -06:00
Patrick Lühne 5c504bef5b
Format positive result more nicely 2019-11-07 02:25:01 -06:00
Patrick Lühne 33c5245b80
Skip input predicates in completion 2019-11-07 02:17:49 -06:00
Patrick Lühne a802b9f8fd
Rename Statement to FormulaStatement 2019-11-07 01:12:26 -06:00
Patrick Lühne a206812d80
Implement forward and backward proofs with all new directives correctly 2019-11-07 00:53:50 -06:00
Patrick Lühne cf90f4f69a
Don’t rewrite specification files for now 2019-11-06 23:24:25 -06:00
Patrick Lühne 2d7f9db378
Improve output 2019-11-06 22:43:22 -06:00
Patrick Lühne 2411781728
Add lemma directives 2019-11-06 22:42:42 -06:00
Patrick Lühne e933c45079
Tag completion directives with source 2019-11-06 21:20:06 -06:00
Patrick Lühne 39a047e10a
Show Vampire proof times 2019-11-06 19:05:15 -06:00
Patrick Lühne fa2110294a
Support right-to-left implications 2019-11-06 19:05:04 -06:00
Patrick Lühne 7da722aeec
Implement backward proofs 2019-11-06 12:52:08 -06:00
Patrick Lühne bce9d8061c
Verify all assertions one after the other 2019-11-06 04:36:51 -06:00
Patrick Lühne 3bf78115cf
Add completion, assumption, and assertion directives 2019-11-06 00:18:30 -06:00
Patrick Lühne beb4dbb693
Fix TPTP output of predicates with arguments 2019-11-05 15:54:28 -06:00
Patrick Lühne 3c94f677fc
Update foliage 2019-11-05 15:54:09 -06:00
Patrick Lühne 199afd6768
Fix variable names in TPTP 2019-11-05 13:58:21 -06:00
Patrick Lühne 2a8a076ecd
Fix precedence rules for subtractions and implications 2019-11-05 13:15:13 -06:00
Patrick Lühne 56ed5f1cf1
Recognize program variables better 2019-11-05 12:54:38 -06:00
Patrick Lühne b0173a7b9a
Support comments and don’t touch input more than necessary 2019-11-05 12:44:28 -06:00
Patrick Lühne cc56c493f6
Add stderr to error output 2019-11-02 07:54:39 +01:00
Patrick Lühne 0d63e48af9
Fix typos 2019-11-02 07:54:29 +01:00
Patrick Lühne 52d8c84bc0
Finish first version of interactive prover 2019-11-02 07:23:47 +01:00
Patrick Lühne 228b2032f7
Make anthem axiomatization more consistent 2019-11-02 05:07:05 +01:00
Patrick Lühne e382058c2d
Add missing anthem axioms 2019-11-02 04:13:14 +01:00
Patrick Lühne 306dc7d850
Fix typos 2019-11-02 03:13:51 +01:00
Patrick Lühne a93af5b423
Print TPTP type directives for predicates 2019-11-02 02:57:20 +01:00
Patrick Lühne 00169b2144
Handle comparisons with nonarithmetic terms 2019-11-02 02:26:56 +01:00
Patrick Lühne 7d47910cfa
Initial project file parser 2019-11-02 02:13:45 +01:00