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

Conversation

SimonGuilloud
Copy link
Collaborator

Reimplement Lisa's syntax to include lambda expressions over first order logic.
This will allow, for example, to write directly and efficiently anonymous functions and set comprehensions.

SimonGuilloud and others added 30 commits October 8, 2024 18:25
@SimonGuilloud
Reimplemented syntax and OL equivalence checker.
26e3b86
@SimonGuilloud
Added Sequent calculus and proofs, but not yet proof checking.
690a9de
@SimonGuilloud
Finished proof checker, have to deal with definitions and beta reduti…
8747557 
…ons.
@SimonGuilloud
Mostly finished Kernel, left with Beta and epsilon rules.
f62a926
@SimonGuilloud
Update Kernel helper, serialization, and more.
414f027 
Next step: rest of TPTP parsing, utils.fol, utils.prooflib.
@SimonGuilloud
refactor and move temp files
1486fa3
@SimonGuilloud
add missing files
f38067f
@SimonGuilloud
update the sctptp parser
bbeffa5
@SimonGuilloud
POrted most of top-level syntax
256fd44
@SimonGuilloud
Finished top-level syntax, including sequents. Next: Prooflib
2b790af
@SimonGuilloud
Mosly finished with prooflib, currently doing definitions. Remains Ba…
b6ffb85 
…sicStepTactics for beta conversion.
@SimonGuilloud
At this stage, compiles but many things left commented to track the bug.
ccbe7f0
@SimonGuilloud
all of utils except for UnificationUtils ported. Next, tests.
02665e8
@sankalpgambhir
Seal fol.Expr
22c3de6
@sankalpgambhir
Basic matching
9239dce
@sankalpgambhir
Document matchExpr
7a9e672
@sankalpgambhir
Implement Substitution
a01ac26
@sankalpgambhir
Define a rewrite context
b5c8bd2
@sankalpgambhir
Use OL eq, correctly check whether subst respects bound vars
db8f973
@sankalpgambhir
scalafmt
c76eb21
@sankalpgambhir
typo
1eec816
@SimonGuilloud
lisa-utils tests compile
aa4045d
@SimonGuilloud
Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol
c9f37c6
@SimonGuilloud
Some tests pass.
6e06964
@SimonGuilloud
utils tests passing. Left to do:
ee6d5b6 
- BasicTacticTest
- UnificationTest
- printer and parsers test: Port to TPTP-based printer (longer term)
@SimonGuilloud
ongoing work on tautology
3ebc3a8
@SimonGuilloud
Tautology and Tableaux compile. Experiments with unapply paterns in l…
e4c3036 
…isa.utils.fol.
@sankalpgambhir
Change depth to not recalculate
248059c
@SimonGuilloud
small corrections to subst steps in basic step tactics and kernel, on…
1f671c4 
…going portage of congruence.
@SimonGuilloud
Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol
d69ffe4
sankalpgambhir and others added 30 commits October 29, 2024 12:13
@sankalpgambhir
Fix proof reconstruction to use instantiated rewrite rules
7bce89d
@SimonGuilloud
Update proof parser to handle substitution step. Correct bug in equiv…
13a6946 
…alence checker. Other minor improvements.
@SimonGuilloud
Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol
b92ae33
@SimonGuilloud
add goeland files in sets2
91ee02b
@SimonGuilloud
small improvements.
f624c6a
@SimonGuilloud
Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol
bce732c
@sankalpgambhir
Add ID counter
7c8aa45
@sankalpgambhir
Fully qualify Definition for now
a497bb6
@sankalpgambhir
Add new WIP extensionality and upair theorems
7d2a95c
@SimonGuilloud
fix bug in Tautology
09de0ed
@sankalpgambhir
Only compute base sequent once in extensionality
879d83d
@sankalpgambhir
Save wip set theory library
24b9329
@sankalpgambhir
Add emptiness check for max id calculation in rewriting
f16e268
@sankalpgambhir
Remove print in singleton
794fcf8
@sankalpgambhir
Add comprehension
ccc5e17
@sankalpgambhir
Add simple list printer
bb7ebb5
@sankalpgambhir
Add quantifyAll tactic
c0b391c
@sankalpgambhir
Remove unused targetName import
b3818cf
@sankalpgambhir
Add transitivity proof
2e5dcd3
@sankalpgambhir
Add replacement definition
f9f64cf
@sankalpgambhir
Add replacement proofs
4f6f28d
@sankalpgambhir
Add parenthesies to fix equality parsing
75f4c74
@sankalpgambhir
Clean up quantifyAll documentation
ff40c93
@sankalpgambhir
Add RightEpsilon scaffold
d39c480
@sankalpgambhir
Remove subproof for uniformity
2a72d75
@sankalpgambhir
Remove unnecessary condition in RightEpsilon docs
ef9c12c
@sankalpgambhir
Add RightEpsilon.withParameters
87f5e45
@sankalpgambhir
Clarify type in Binder.unapply
cb318da
@sankalpgambhir
Parameter inference for RightEpsilon
4659dfe
@sankalpgambhir
Change _ to null per compiler warning suggestion
ef31631
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@SimonGuilloud @sankalpgambhir