Kaustuv Chaudhuri chaudhuri

Organizations

abella-prover
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 2d1410b
    ProofCert-capable output?
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 8f9a407
    Fix parsing issues with ~ and <=>
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri ce95b20
    Changed the precedence of <=> to be lowest
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 89b1c59
    New flag to play with EVC on Pseudos
Kaustuv Chaudhuri
SYN053+1.mg makes maetning hang unexpectedly.
chaudhuri commented on issue chaudhuri/maetning#3
Kaustuv Chaudhuri

This is no longer problematic, but I forgot to note down what fixed it. Maybe d4a8532 ?

Kaustuv Chaudhuri
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri f029816
    COMPLETENESS : evc test now ignores pseudo labels
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri d0eaef9
    Add <=> as a syntactic sugar for a bi-implication.
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri d4a8532
    SOUNDNESS : the e.v.c. must ensure distinctness of e.v.s
chaudhuri commented on issue chaudhuri/maetning#3
Kaustuv Chaudhuri

The issue here is that percolation is spinning with copies of existing rules. I got the loops backwards. It is for every active for every rule, not…

Kaustuv Chaudhuri
  • Kaustuv Chaudhuri bfac8f4
    SOUNDNESS: iterated matching was accidentally unifying
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 47e37e6
    SOUNDNESS : rule conclusion labels incorrectly tweaked for locals
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 2a92df9
    Updating copyright and Inria sigils
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 0404ba8
    Added sum example from Taus
Kaustuv Chaudhuri
Kaustuv Chaudhuri
Rules that create new variables break saturation
chaudhuri commented on issue chaudhuri/maetning#2
Kaustuv Chaudhuri

Appears to be the same as #1.

Kaustuv Chaudhuri
Rules that create new variables break saturation
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 8409b84
    OTTER loop: only percolate new rules, not all rules
Kaustuv Chaudhuri
Quiescence issue with new_rules
Kaustuv Chaudhuri
Quiescence issue with new_rules
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri c6a43e6
    Track the terms of the pseudo instances in the labels
Kaustuv Chaudhuri
Kaustuv Chaudhuri
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri a6f0404
    Finished a first cut of the frontend.
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 5135f4f
    Add the beginnings of a frontend.
Kaustuv Chaudhuri
  • Kaustuv Chaudhuri 9c5e618
    Was generating too many initial sequents.