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

Add lambda-terms to FOL #231

Draft
wants to merge 59 commits into
base: main
Choose a base branch
from
Draft

Add lambda-terms to FOL #231

wants to merge 59 commits into from

Commits on Oct 8, 2024

  1. Reimplemented syntax and OL equivalence checker.

    @SimonGuilloud
    SimonGuilloud committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    26e3b86 View commit details
    Browse the repository at this point in the history

  2. Added Sequent calculus and proofs, but not yet proof checking.

    @SimonGuilloud
    SimonGuilloud committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    690a9de View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. Finished proof checker, have to deal with definitions and beta reduti… 

    …ons.
    @SimonGuilloud
    SimonGuilloud committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    8747557 View commit details
    Browse the repository at this point in the history

  2. Mostly finished Kernel, left with Beta and epsilon rules.

    @SimonGuilloud
    SimonGuilloud committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    f62a926 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2024

  1. Update Kernel helper, serialization, and more. 

    Next step: rest of TPTP parsing, utils.fol, utils.prooflib.
    @SimonGuilloud
    SimonGuilloud committed Oct 11, 2024
    Configuration menu
    Copy the full SHA
    414f027 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2024

  1. refactor and move temp files

    @SimonGuilloud
    SimonGuilloud committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    1486fa3 View commit details
    Browse the repository at this point in the history

  2. add missing files

    @SimonGuilloud
    SimonGuilloud committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    f38067f View commit details
    Browse the repository at this point in the history

  3. update the sctptp parser

    @SimonGuilloud
    SimonGuilloud committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    bbeffa5 View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2024

  1. POrted most of top-level syntax

    @SimonGuilloud
    SimonGuilloud committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    256fd44 View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2024

  1. Finished top-level syntax, including sequents. Next: Prooflib

    @SimonGuilloud
    SimonGuilloud committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    2b790af View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2024

  1. Mosly finished with prooflib, currently doing definitions. Remains Ba… 

    …sicStepTactics for beta conversion.
    @SimonGuilloud
    SimonGuilloud committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    b6ffb85 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2024

  1. At this stage, compiles but many things left commented to track the bug.

    @SimonGuilloud
    SimonGuilloud committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    ccbe7f0 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. all of utils except for UnificationUtils ported. Next, tests.

    @SimonGuilloud
    SimonGuilloud committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    02665e8 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. Seal fol.Expr

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    22c3de6 View commit details
    Browse the repository at this point in the history

  2. Basic matching

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    9239dce View commit details
    Browse the repository at this point in the history

  3. Document matchExpr

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    7a9e672 View commit details
    Browse the repository at this point in the history

  4. Implement Substitution

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    a01ac26 View commit details
    Browse the repository at this point in the history

  5. Define a rewrite context

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    b5c8bd2 View commit details
    Browse the repository at this point in the history

  6. Use OL eq, correctly check whether subst respects bound vars

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    db8f973 View commit details
    Browse the repository at this point in the history

  7. scalafmt

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    c76eb21 View commit details
    Browse the repository at this point in the history

  8. typo

    @sankalpgambhir
    sankalpgambhir committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    1eec816 View commit details
    Browse the repository at this point in the history

  9. lisa-utils tests compile

    @SimonGuilloud
    SimonGuilloud committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    aa4045d View commit details
    Browse the repository at this point in the history

  10. Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol

    @SimonGuilloud
    SimonGuilloud committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    c9f37c6 View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2024

  1. Some tests pass.

    @SimonGuilloud
    SimonGuilloud committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    6e06964 View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2024

  1. utils tests passing. Left to do: 

    - BasicTacticTest
- UnificationTest
- printer and parsers test: Port to TPTP-based printer (longer term)
    @SimonGuilloud
    SimonGuilloud committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    ee6d5b6 View commit details
    Browse the repository at this point in the history

  2. ongoing work on tautology

    @SimonGuilloud
    SimonGuilloud committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    3ebc3a8 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2024

  1. Tautology and Tableaux compile. Experiments with unapply paterns in l… 

    …isa.utils.fol.
    @SimonGuilloud
    SimonGuilloud committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    e4c3036 View commit details
    Browse the repository at this point in the history

Commits on Oct 23, 2024

  1. Change depth to not recalculate

    @sankalpgambhir
    sankalpgambhir committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    248059c View commit details
    Browse the repository at this point in the history

  2. small corrections to subst steps in basic step tactics and kernel, on… 

    …going portage of congruence.
    @SimonGuilloud
    SimonGuilloud committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    1f671c4 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol

    @SimonGuilloud
    SimonGuilloud committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    d69ffe4 View commit details
    Browse the repository at this point in the history

  4. Continued work on congruence actic.

    @SimonGuilloud
    SimonGuilloud committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    f0935cf View commit details
    Browse the repository at this point in the history

  5. Return substitution to first and second order only.

    @SimonGuilloud
    SimonGuilloud committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    3bfce57 View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

  1. general improvements, update to congruence.

    @SimonGuilloud
    SimonGuilloud committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    516ef5b View commit details
    Browse the repository at this point in the history

  2. Change memoized internals to be protected instead of private

    @sankalpgambhir
    sankalpgambhir committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    ea67c79 View commit details
    Browse the repository at this point in the history

  3. Readd collectFirstDefined function, make utils.collection

    @sankalpgambhir
    sankalpgambhir committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    146c074 View commit details
    Browse the repository at this point in the history

  4. Make Substitution class more reliable

    @sankalpgambhir
    sankalpgambhir committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    2d04ee9 View commit details
    Browse the repository at this point in the history

  5. Make LeftForall and RightExists use new matching

    @sankalpgambhir
    sankalpgambhir committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    8917298 View commit details
    Browse the repository at this point in the history

  6. Congruence.scala compiles

    @SimonGuilloud
    SimonGuilloud committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    47c1035 View commit details
    Browse the repository at this point in the history

  7. update SetTheoryLibrary, small improvement to Syntax.scala unapply.

    @SimonGuilloud
    SimonGuilloud committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    261a9cb View commit details
    Browse the repository at this point in the history

  8. debugging pettern matching

    @SimonGuilloud
    SimonGuilloud committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    f62d9cc View commit details
    Browse the repository at this point in the history

  9. clean to sets2. 

    clean to sets2.
    @SimonGuilloud
    SimonGuilloud committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    343b810 View commit details
    Browse the repository at this point in the history

  10. fix bugs in equivalence checker and Tableau.

    @SimonGuilloud
    SimonGuilloud committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    874c3ce View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

  1. Rewrite Substitution.Apply

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    d147215 View commit details
    Browse the repository at this point in the history

  2. Add toOptionSeq extension method

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    2c23d19 View commit details
    Browse the repository at this point in the history

  3. Add andAll / orAll methods

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    7e6e89a View commit details
    Browse the repository at this point in the history

  4. Switch tactic inputs to use Seq instead of List

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    c14b35f View commit details
    Browse the repository at this point in the history

  5. Extend RewriteContext with rules

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    792f904 View commit details
    Browse the repository at this point in the history

  6. Better matching documentation and naming

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    d3a6d26 View commit details
    Browse the repository at this point in the history

  7. Rewrite method and classes scaffolds

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4e621fc View commit details
    Browse the repository at this point in the history

  8. Minor corrections

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    fc29f49 View commit details
    Browse the repository at this point in the history

  9. Upgrade to scala 3.5.2

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    1ea1a11 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'lambdafol2' into lambdafol

    @SimonGuilloud
    SimonGuilloud committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5089f70 View commit details
    Browse the repository at this point in the history

  11. add some @unchecked, git add new lisa-sets2 folder.

    @SimonGuilloud
    SimonGuilloud committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    1d1cbc3 View commit details
    Browse the repository at this point in the history

  12. reestablish a vompilation crash for tests.

    @SimonGuilloud
    SimonGuilloud committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    cd05987 View commit details
    Browse the repository at this point in the history

  13. small fix

    @SimonGuilloud
    SimonGuilloud committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    d369a7e View commit details
    Browse the repository at this point in the history

  14. Add new Vector backed order-preserving Set

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    929d8e4 View commit details
    Browse the repository at this point in the history

  15. Expand rewrite result types

    @sankalpgambhir
    sankalpgambhir committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5ab7342 View commit details
    Browse the repository at this point in the history

  16. Improve pretty printing

    @SimonGuilloud
    SimonGuilloud committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5f6de32 View commit details
    Browse the repository at this point in the history

  17. Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol

    @SimonGuilloud
    SimonGuilloud committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    17e1dfb View commit details
    Browse the repository at this point in the history