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

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
SimonGuilloud and others added 29 commits October 23, 2024 20:37
@SimonGuilloud
Continued work on congruence actic.
f0935cf
@SimonGuilloud
Return substitution to first and second order only.
3bfce57
@SimonGuilloud
general improvements, update to congruence.
516ef5b
@sankalpgambhir
Change memoized internals to be protected instead of private
ea67c79
@sankalpgambhir
Readd collectFirstDefined function, make utils.collection
146c074
@sankalpgambhir
Make Substitution class more reliable
2d04ee9
@sankalpgambhir
Make LeftForall and RightExists use new matching
8917298
@SimonGuilloud
Congruence.scala compiles
47c1035
@SimonGuilloud
update SetTheoryLibrary, small improvement to Syntax.scala unapply.
261a9cb
@SimonGuilloud
debugging pettern matching
f62d9cc
@SimonGuilloud
clean to sets2.
343b810 
clean to sets2.
@SimonGuilloud
fix bugs in equivalence checker and Tableau.
874c3ce
@sankalpgambhir
Rewrite Substitution.Apply
d147215
@sankalpgambhir
Add toOptionSeq extension method
2c23d19
@sankalpgambhir
Add andAll / orAll methods
7e6e89a
@sankalpgambhir
Switch tactic inputs to use Seq instead of List
c14b35f
@sankalpgambhir
Extend RewriteContext with rules
792f904
@sankalpgambhir
Better matching documentation and naming
d3a6d26
@sankalpgambhir
Rewrite method and classes scaffolds
4e621fc
@sankalpgambhir
Minor corrections
fc29f49
@sankalpgambhir
Upgrade to scala 3.5.2
1ea1a11
@SimonGuilloud
Merge branch 'lambdafol2' into lambdafol
5089f70
@SimonGuilloud
add some @unchecked, git add new lisa-sets2 folder.
1d1cbc3
@SimonGuilloud
reestablish a vompilation crash for tests.
cd05987
@SimonGuilloud
small fix
d369a7e
@sankalpgambhir
Add new Vector backed order-preserving Set
929d8e4
@sankalpgambhir
Expand rewrite result types
5ab7342
@SimonGuilloud
Improve pretty printing
5f6de32
@SimonGuilloud
Merge branch 'lambdafol' of github.com:SimonGuilloud/lisa into lambdafol
17e1dfb
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