search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

It should be possible to export and import LISA proofs into and from text files. #76

Closed SimonGuilloud closed 10 months ago

SimonGuilloud commented 1 year ago

It should be possible to export LISA's kernel proof unambiguously to text files, and import them back Suggested format:

#2 |- A => A by Subproof with -1, -3 {
       #2.-2 X by Import
       #2.-1 Y by Import
        #2.0 Z by LeftImplies with A
}
#3 |- B by Cut 0, 1 with phi
SimonGuilloud commented 10 months ago

We can do so into binary files with serialization since https://github.com/epfl-lara/lisa/pull/187