ComputerAidedLL click-and-collect issues

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

16 stars 2 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Proof nets

#174 suhr opened 1 year ago
2
[Parsing] Make multiplicative connectives more associative than additive ones

#173 olaure01 opened 2 years ago
0
Cut-elimination on open proofs may change the order of formulas in open leaves

#172 olaure01 opened 2 years ago
0
Errors in the auto-prover with top

#171 Shurtugal opened 2 years ago
0
Technical Error

#170 Nick-Munnich opened 2 years ago
0
Feature proposal : update proof when exchanging hypotheses

#169 emiquey opened 2 years ago
2
Going back to the beginning of a cut-elimination sequence

#168 KostiaChardonnet opened 2 years ago
0
[Coq] nanoyalla.zip unreachable

#167 olaure01 closed 2 years ago
1
[Cut elimination] error message when reducing (probably due to exchange)

#166 olaure01 closed 2 years ago
0
Exchange management inside proofs

#165 olaure01 opened 2 years ago
3
Highlight ancestors and descendants in transformation mode

#164 etiennecallies opened 2 years ago
8
Proof transformation: double click on reversible formula

#163 etiennecallies opened 2 years ago
0
Url parameters

#162 olaure01 closed 2 years ago
1
[Cut] Dedicated color for cut formulas

#161 olaure01 closed 2 years ago
1
Link to derivation rules broken

#160 olaure01 closed 3 years ago
1
Proof grafting

#159 olaure01 opened 3 years ago
0
Apply reversible first

#158 etiennecallies closed 2 years ago
5
Cut elimination messages. Fixes #148

#157 etiennecallies closed 3 years ago
1
highlight cut formula fixes #149

#156 etiennecallies closed 3 years ago
0
Simplify proof button

#155 etiennecallies closed 3 years ago
1
[auto-prover] exchange rule displayed

#154 olaure01 closed 3 years ago
0
[Substitution] Substitution with definition

#153 olaure01 closed 3 years ago
0
[Full axiom expansion] error

#152 olaure01 closed 3 years ago
0
[simplify proof] Too strong

#151 olaure01 closed 3 years ago
0
[cut elimination] eliminate-all button not re-initialized with undo

#150 olaure01 closed 3 years ago
0
highlight cut formula

#149 lionelvaux closed 3 years ago
2
Display more information on cut elimination rules to be applied

#148 lionelvaux closed 3 years ago
0
Cut elimination

#147 etiennecallies closed 3 years ago
2
[cut elimination] error: invalid proof

#146 olaure01 closed 3 years ago
0
[undo-redo] History should be cleared when leaving proof-transformation mode

#145 olaure01 closed 3 years ago
0
[cut elimination] explicit exchange appearing

#144 olaure01 closed 3 years ago
3
Proof-transformation mode vs other options

#143 olaure01 opened 3 years ago
1
Axiom expansion

#142 etiennecallies closed 3 years ago
2
No provability check when acyclic notations. Fixes #139

#141 etiennecallies closed 3 years ago
1
UTF-8 headers

#140 etiennecallies closed 3 years ago
2
[Provability checks] Empty sequent may be provable with cuts and cyclic notations

#139 olaure01 closed 3 years ago
2
export permutation to latex explicit exchanges

#138 etiennecallies closed 3 years ago
0
[MAJOR REFACTORING] Switch to opium

#137 etiennecallies closed 3 years ago
0
[Notations] extend text exports with notations

#136 olaure01 closed 3 years ago
1
Fix stack overflow

#135 etiennecallies closed 3 years ago
2
[Cyclic Notation] Autoprover generates error

#134 olaure01 closed 3 years ago
1
Help notations

#133 etiennecallies closed 3 years ago
0
[Notation] Larger field for notation name

#132 olaure01 closed 3 years ago
1
Auto-prover with cyclic notations

#131 etiennecallies closed 3 years ago
1
[Coq] rewrite tactic for cyclic notations

#130 olaure01 closed 3 years ago
1
Help on notations

#129 olaure01 closed 3 years ago
0
Auto-prover on sequent using recursive notations

#128 etiennecallies closed 3 years ago
4
Auto-prover with non-recursive notations

#127 etiennecallies closed 3 years ago
4
[Notation] initial provability check

#126 olaure01 closed 3 years ago
1
[Notation] do not auto-reverse defined axioms

#125 olaure01 closed 3 years ago
0