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
[Cut elimination] error message when reducing (probably due to exchange) #166
Closed
olaure01 closed 3 years ago
Reducing the cut in the following proof generates an error (
Technical error...): https://click-and-collect.linear-logic.org/?s=A%5E%2CA&proofTransformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl5TNc9IpsMO0FeJWvwtztFN7zEMS9TQmmXROQc%2F88tyS8v9zc4Dow2AbH7Ja6n%2Fm4fFMqaJo5o7P2vFwXJqBvv6RRBkARKefooEU5hQuOZDMfXjGfatcaD%2FgkRxms4mMRoUBTqXNlARw%2F9UENI3G3PF2wVB8sfxlTq3EW%2BH2d9W0JgR0iZ5Xt7K%2BRHSxHAZ3hvuB9Oasn5oI4bLnbdOytGBRaCqJGqOCy0OYKmcV9ubENPJ%2BhLhngu3xy1vaL9VbzoVwUPpinEjykO3sO5cqGufvW%2Bi97zInE%2F723TU%3D (but not if simplification is applied first).