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
[auto-prover] exchange rule displayed #154
Closed
olaure01 closed 3 years ago
Running the automatic prover on the premise of: http://localhost:3000/?s=A%5E*B%5E%2CA%7CB&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzmB%2ForC2WnFSzdubJ856ioYOWgHbegtOz4PKXx7TIYuvxXqz0MeI3hRv9iZaXC2lpiKS5oKuMBI6Ej59sZs2zBFUdW7p%2FjP7JE1pwYbNzqnNDn7E%2FuOLzsKZ0D5CyflDRSnO3jd1wM82nOxT7FZL32cWggWEHjPA%2Fb4%2B99RZRu4mpx6g3OJy2vgApKZsyPFb9eV84 generates an explicit exchange rule. (this problem occurs on pre-prod and development versions, not on prod)