Commits · disjunction · Iris / Diaframe

13 May, 2022 2 commits
- paper · fb8dcacd
  Łukasz Czajka authored May 13, 2022
  
  fb8dcacd
- paper: related work · b6edecde
  Łukasz Czajka authored May 13, 2022
  
  b6edecde
12 May, 2022 3 commits
- paper · 6f505f5a
  Łukasz Czajka authored May 12, 2022
  
  6f505f5a
- paper · e641f6a3
  Łukasz Czajka authored May 12, 2022
  
  e641f6a3
- paper · 579c5b39
  Łukasz Czajka authored May 12, 2022
  
  579c5b39
29 Apr, 2022 1 commit
- fixes · e77369ad
  Łukasz Czajka authored Apr 29, 2022
  
  e77369ad
28 Apr, 2022 1 commit
- remove biabd_instances_disj.v · b89095e6
  Łukasz Czajka authored Apr 28, 2022
  
  b89095e6
22 Apr, 2022 3 commits
- existentials under disjunction · 96765a7c
  Łukasz Czajka authored Apr 22, 2022
  
  96765a7c
- right/left disjunction focusing hints · 8034598d
  Łukasz Czajka authored Apr 22, 2022
  
  8034598d
- refactoring · 65ee116b
  Łukasz Czajka authored Apr 22, 2022
  
  65ee116b
21 Apr, 2022 1 commit
- New abduct hint search working on examples, existential problem seems fixed. · f7529f5a
  Ike Mulder authored Apr 21, 2022
  
  f7529f5a
15 Apr, 2022 4 commits
- Merge branch 'disjunction' of gitlab.mpi-sws.org:iris/diaframe into disjunction · ff91e61c
  Ike Mulder authored Apr 15, 2022
  
  ff91e61c
- Some progress on abduct hint search. · 5963186c
  Ike Mulder authored Apr 15, 2022
  
  5963186c
- rules.tex · 620b1fad
  Łukasz Czajka authored Apr 15, 2022
  
  620b1fad
- SolveSepFoc and solvePure · 14268312
  Łukasz Czajka authored Apr 15, 2022
  
  14268312
07 Apr, 2022 2 commits
- Added base abdatomdisj instance and solveonefoc rule. · bf653735
  Ike Mulder authored Apr 07, 2022
  
  bf653735
- Alternative definition of abductdisj, proved interaction with solveone. · 2f563771
  Ike Mulder authored Apr 07, 2022
  
  2f563771
31 Mar, 2022 1 commit
- normalize disjunctions · c2630edf
  Łukasz Czajka authored Mar 31, 2022
  
  c2630edf
25 Mar, 2022 1 commit
- SolveOneFoc · be522c15
  Łukasz Czajka authored Mar 25, 2022
  
  be522c15
24 Mar, 2022 1 commit
- Shortened some proofs now AbdDisj takes a boolean. · 6f617588
  Ike Mulder authored Mar 24, 2022
  
  6f617588
23 Mar, 2022 6 commits
- Merge branch 'disjunction' of https://gitlab.mpi-sws.org/iris/diaframe into disjunction · 2d64dbc7
  Łukasz Czajka authored Mar 23, 2022
  
  2d64dbc7
- disj_test.v · 837710ee
  Łukasz Czajka authored Mar 23, 2022
  
  837710ee
- Merge branch 'disjunction' of gitlab.mpi-sws.org:iris/diaframe into disjunction · 13da5791
  Ike Mulder authored Mar 23, 2022
  
  13da5791
- Merge branch 'disjunction' of gitlab.mpi-sws.org:iris/diaframe into disjunction · 4ff02c1e
  Ike Mulder authored Mar 23, 2022
  
  4ff02c1e
- AbductDisj fix handling of disjunctions on the left · c382bc2e
  Łukasz Czajka authored Mar 23, 2022
  
  c382bc2e
- Added stronger version of SolveSepFoc, hint search for BiAbdDisj2 now working,... · 4979e0f8
  Ike Mulder authored Mar 23, 2022
```
Added stronger version of SolveSepFoc, hint search for BiAbdDisj2 now working, solves existential problem in various cases.
```
  4979e0f8
22 Mar, 2022 3 commits
- AbductDisj · 62151ba5
  Łukasz Czajka authored Mar 22, 2022
  
  62151ba5
- AbductDisj backward-compatible · 07025842
  Łukasz Czajka authored Mar 22, 2022
  
  07025842
- Working on moving to alternative BiAbdDisj2 definition, fixes parts of existential problem. · 99155206
  Ike Mulder authored Mar 22, 2022
  
  99155206
21 Mar, 2022 2 commits
- comparison fixes · 1f36fb65
  Łukasz Czajka authored Mar 21, 2022
  
  1f36fb65
- fix compilation · f83287c5
  Łukasz Czajka authored Mar 21, 2022
  
  f83287c5
10 Mar, 2022 4 commits
- Proved all necessary lemmas (I think), now to make it into a tactic. · fb104a13
  Ike Mulder authored Mar 10, 2022
  
  fb104a13
- Laying groundwork for biabddisj with extra telescope. · de7fdf9f
  Ike Mulder authored Mar 10, 2022
  
  de7fdf9f
- Focused problematic invocations of iStepS. · 43d11dfb
  Ike Mulder authored Mar 10, 2022
  
  43d11dfb
- Fix priority of modality instances. · e2af484e
  Ike Mulder authored Mar 10, 2022
  
  e2af484e
08 Mar, 2022 1 commit
- bugfix in search_abd_disj · 3b367029
  Łukasz Czajka authored Mar 08, 2022
  
  3b367029
07 Mar, 2022 2 commits
- fixed search_abd_disj · 5f04f622
  Łukasz Czajka authored Mar 07, 2022
  
  5f04f622
- fix bug with conjunction in iStepS · 8a3ba357
  Łukasz Czajka authored Mar 07, 2022
  
  8a3ba357
21 Feb, 2022 1 commit
- first version of solveOneStepDisj (breaks things) · f4a4b093
  Łukasz Czajka authored Feb 21, 2022
  
  f4a4b093
13 Jan, 2022 1 commit
- Got most examples working, with some caveats. · 3c5fc7cd
  Ike Mulder authored Jan 13, 2022
  
  3c5fc7cd