search

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

[simplify proof] Too strong #151

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

Simplify button should only apply transformations which do not modify the semantics.

On: http://ccll.linear-logic.org/?s=n&n=n%2C1+%2B+n&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslSkmUUdC6wcpw%2BxPIisUM%2FDU96uPUsSW4WGq29bgUwwGLR5eRh%2BVD8DkMojLvBUaM6QT1Jmah2RSdgTk5pB3DOxBPj0OTqTrghQwGwi0TIjY3WT%2Ba4V0lpEMJ%2FrP9%2B9AhoJrhNgItgMScxk%2BRhXJ%2FJW9ZCe3%2F2PKjiLwkfBnPDr1X3wNPi0iuwSftixf%2F8bQRCE%3D Simplify turns the encoding of 1 into the encoding of 0. Loop detection should be avoided.