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

Add lambda-terms to FOL #231

wants to merge 129 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 November 6, 2024 11:11
@sankalpgambhir
Remove T and F sorts. Merge some Sort / Expr[Sort] handling.
a195714
@sankalpgambhir
scalafmt
1645dd3
@sankalpgambhir
Fix lisa-utils tests
c82e4b2
@sankalpgambhir
Remove old Substitution code
0d1ba1f
@sankalpgambhir
Add ExprOps
8cba55b
@sankalpgambhir
Remove unnecessary argument reversal in DEF
dd5850b
@sankalpgambhir
Correctly factor lisa.utils subpackages
08de69d
@sankalpgambhir
Make collect type more precise
b23f197
@sankalpgambhir
Make Binder.unapply type less precise
9b8e78f
@sankalpgambhir
Implement collectEpsilons
2a71ded
@sankalpgambhir
Reflip accidental flipping of pivot and target in RightEpsilon
70087d3
@sankalpgambhir
Correctly add flipped rules for rewriting as well
d974f4a
@sankalpgambhir
Correctly compute violating pairs for error reporting in rewriting
3e52f43
@sankalpgambhir
Better error reporting for Substitution.Apply
4cfd504
@sankalpgambhir
Fix runtime error for not-specific-enough cast
7d62d26
@sankalpgambhir
Change printList separator to prefix
28e97f1
@SimonGuilloud
add support for Egg
425b41e
@SimonGuilloud
add Egg.scala
3a3a865
@SimonGuilloud
Add support for egg and egg executable for windows.
2baf58b
@SimonGuilloud
clean Test.scala
bab6ed1
@sankalpgambhir
Correctly discharge direction-swapped rules in Substitution
5edb62a
@sankalpgambhir
Correctly instantiate definitions in Comprehension proof
dd8585a
@sankalpgambhir
Allow construction of variables from identifiers unsafely
ddf1b64
@sankalpgambhir
Reimplement capture avoiding substitution on abstraction terms
583eced
@sankalpgambhir
Correctly substitute in transitivity proof
54bc570
@sankalpgambhir
Correct replacement proof
fb0250b
@sankalpgambhir
Fix quantifyAll, make it a proper tactic
3611a5e
@sankalpgambhir
Cleanup RightEpsilon
4a7c75c
@SimonGuilloud
smal update to Egg.scala.
0a61afd
@SimonGuilloud
Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol
ff44367
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