Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Simplify (generalised) invertible rules in Δ in E(Δ) and A(Δ, φ) #31

Merged
merged 14 commits into from
Sep 11, 2024
Merged

Simplify (generalised) invertible rules in Δ in E(Δ) and A(Δ, φ) #31

merged 14 commits into from
Sep 11, 2024

Commits on Aug 30, 2024

  1. Add a weight-preserving simplification during PropQuant computation

    @hferee
    hferee committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    ab680b9 View commit details
    Browse the repository at this point in the history

Commits on Sep 3, 2024

  1. Decision procedure for iSL

    @hferee
    hferee committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    15dc02f View commit details
    Browse the repository at this point in the history

  2. Extract the iSL decision procedure to OCaml

    @hferee
    hferee committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    0e5b662 View commit details
    Browse the repository at this point in the history

  3. Decision procedure: name cleanup

    @hferee
    hferee committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    8521f2f View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2024

  1. Compute interpolants by apply invertible rules first ; proofs missing

    @hferee
    hferee committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    8c0a2fb View commit details
    Browse the repository at this point in the history

  2. decorrelate E and A

    @hferee
    hferee committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    d76ad48 View commit details
    Browse the repository at this point in the history

  3. Remove extra formula argument from E

    @hferee
    hferee committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    5df78ae View commit details
    Browse the repository at this point in the history

  4. make progress in defining a correct simplification for environments, … 

    …interleaved during the computation of Pitts Interpolants
    @hferee
    hferee committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    b9fcb92 View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

  1. stash progress on simplification

    @hferee
    hferee committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    c3ceeca View commit details
    Browse the repository at this point in the history

  2. fix definition for env_order_ 

    refl
    @hferee
    hferee committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    b218377 View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2024

  1. Done simplifying Δ in E(Δ) and A(Δ, φ)

    @hferee
    hferee committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    9cd5481 View commit details
    Browse the repository at this point in the history

  2. typo

    @hferee
    hferee committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    2989ca9 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'main' into inv

    @hferee
    hferee committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    d5acbb3 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'main' into inv

    @hferee
    hferee authored Sep 11, 2024
    Configuration menu
    Copy the full SHA
    54b5253 View commit details
    Browse the repository at this point in the history