29 Commits (master)
 

Author SHA1 Message Date
Patrick Lühne aec76f39cf
Support integer constant declarations 2 years ago
Patrick Lühne 5c504bef5b
Format positive result more nicely 2 years ago
Patrick Lühne 33c5245b80
Skip input predicates in completion 2 years ago
Patrick Lühne a802b9f8fd
Rename Statement to FormulaStatement 2 years ago
Patrick Lühne a206812d80
Implement forward and backward proofs with all new directives correctly 2 years ago
Patrick Lühne cf90f4f69a
Don’t rewrite specification files for now 2 years ago
Patrick Lühne 2d7f9db378
Improve output 2 years ago
Patrick Lühne 2411781728
Add lemma directives 2 years ago
Patrick Lühne e933c45079
Tag completion directives with source 2 years ago
Patrick Lühne 39a047e10a
Show Vampire proof times 2 years ago
Patrick Lühne fa2110294a
Support right-to-left implications 2 years ago
Patrick Lühne 7da722aeec
Implement backward proofs 2 years ago
Patrick Lühne bce9d8061c
Verify all assertions one after the other 2 years ago
Patrick Lühne 3bf78115cf
Add completion, assumption, and assertion directives 2 years ago
Patrick Lühne beb4dbb693
Fix TPTP output of predicates with arguments 2 years ago
Patrick Lühne 3c94f677fc
Update foliage 2 years ago
Patrick Lühne 199afd6768
Fix variable names in TPTP 2 years ago
Patrick Lühne 2a8a076ecd
Fix precedence rules for subtractions and implications 2 years ago
Patrick Lühne 56ed5f1cf1
Recognize program variables better 2 years ago
Patrick Lühne b0173a7b9a
Support comments and don’t touch input more than necessary 2 years ago
Patrick Lühne cc56c493f6
Add stderr to error output 2 years ago
Patrick Lühne 0d63e48af9
Fix typos 2 years ago
Patrick Lühne 52d8c84bc0
Finish first version of interactive prover 2 years ago
Patrick Lühne 228b2032f7
Make anthem axiomatization more consistent 2 years ago
Patrick Lühne e382058c2d
Add missing anthem axioms 2 years ago
Patrick Lühne 306dc7d850
Fix typos 2 years ago
Patrick Lühne a93af5b423
Print TPTP type directives for predicates 2 years ago
Patrick Lühne 00169b2144
Handle comparisons with nonarithmetic terms 2 years ago
Patrick Lühne 7d47910cfa
Initial project file parser 2 years ago