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 98 commits into
base: main
Choose a base branch
from
Draft

Add lambda-terms to FOL #231

wants to merge 98 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

Commits on Oct 26, 2024

  1. fixed dome bugs in tautology.

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

  2. add eta-reduction, corect autologies and definitions.

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

Commits on Oct 27, 2024

  1. various fixes and improvements

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

  2. rename setInfix in printInfix

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

  3. more bug fix and improvements

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

Commits on Oct 28, 2024

  1. Fix substitution types

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

  2. fix tptp printing and goeland tactic

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

Commits on Oct 29, 2024

  1. Specialize VecSet conversions to Seq and Vector

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

  2. Fix rewriting to carry instantiations around properly

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

  3. Fix proof reconstruction to use instantiated rewrite rules

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

  4. Update proof parser to handle substitution step. Correct bug in equiv… 

    …alence checker. Other minor improvements.
    @SimonGuilloud
    SimonGuilloud committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    13a6946 View commit details
    Browse the repository at this point in the history

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

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

Commits on Nov 1, 2024

  1. add goeland files in sets2

    @SimonGuilloud
    SimonGuilloud committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    91ee02b View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2024

  1. small improvements.

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

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

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

Commits on Nov 4, 2024

  1. Add ID counter

    @sankalpgambhir
    sankalpgambhir committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    7c8aa45 View commit details
    Browse the repository at this point in the history

  2. Fully qualify Definition for now

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

  3. Add new WIP extensionality and upair theorems

    @sankalpgambhir
    sankalpgambhir committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    7d2a95c View commit details
    Browse the repository at this point in the history

  4. fix bug in Tautology

    @SimonGuilloud
    SimonGuilloud committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    09de0ed View commit details
    Browse the repository at this point in the history

  5. Only compute base sequent once in extensionality

    @sankalpgambhir
    sankalpgambhir committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    879d83d View commit details
    Browse the repository at this point in the history

  6. Save wip set theory library

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

  7. Add emptiness check for max id calculation in rewriting

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

Commits on Nov 5, 2024

  1. Remove print in singleton

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    794fcf8 View commit details
    Browse the repository at this point in the history

  2. Add comprehension

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

  3. Add simple list printer

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

  4. Add quantifyAll tactic

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

  5. Remove unused targetName import

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

  6. Add transitivity proof

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    2e5dcd3 View commit details
    Browse the repository at this point in the history

  7. Add replacement definition

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

  8. Add replacement proofs

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    4f6f28d View commit details
    Browse the repository at this point in the history

  9. Add parenthesies to fix equality parsing

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    75f4c74 View commit details
    Browse the repository at this point in the history

  10. Clean up quantifyAll documentation

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

  11. Add RightEpsilon scaffold

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

  12. Remove subproof for uniformity

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    2a72d75 View commit details
    Browse the repository at this point in the history

  13. Remove unnecessary condition in RightEpsilon docs

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

  14. Add RightEpsilon.withParameters

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    87f5e45 View commit details
    Browse the repository at this point in the history

  15. Clarify type in Binder.unapply

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

  16. Parameter inference for RightEpsilon

    @sankalpgambhir
    sankalpgambhir committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    4659dfe View commit details
    Browse the repository at this point in the history

  17. Change _ to null per compiler warning suggestion

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