Skip to content

Add lambda-terms to FOL #231

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
Draft
wants to merge 151 commits into
base: main
Choose a base branch
from
Draft

Add lambda-terms to FOL #231

wants to merge 151 commits into from

Conversation

@SimonGuilloud
Copy link
Collaborator

@SimonGuilloud SimonGuilloud commented Oct 8, 2024

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 8, 2024 10:44
@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
@SimonGuilloud
Scaladoc for kernel's FOL, including Syntax and EquivalenceChecker
582d660
@SimonGuilloud
Update documentation and manual
603041b
@SimonGuilloud
Fix a bbug in beta normalization and write scala doc for utils syntax.
f25306f
@SimonGuilloud
Update documentation, what about font syntax in the manual.
ed8dd54
@SimonGuilloud
fix in proof parsing in ProofParser.scala
a213ff4
@SimonGuilloud
add a test for egg.
5b3d99b
@SimonGuilloud
update sctptp parser to latest syntax.
241bda6
@SimonGuilloud
progress on tptp support, fix a bug with eta equivalence.
eefa967
@SimonGuilloud
unfold instForall and RightPrenex for ProofParser
7171f53
@SimonGuilloud
add executables for p9 and goeland (slightly buggy) and corresponding…
d612100 
… tactics.
@SimonGuilloud
remove temp .p files
95547b7
@SimonGuilloud
small fix, update egg exec on windows.
b4b1800
@SimonGuilloud
fix sanitization of variables in tptp proof parser.
f3d5a77
@SimonGuilloud
ad dp9.jar
ca08bf6
@SimonGuilloud
Fixes and update to hammers
7ebd2a9
@SimonGuilloud
update egg-sc-tptp exec.
8c7e24d
@SimonGuilloud
update egg exec and test
3dcccb0
@SimonGuilloud
fix egg exec and tests
84e2020
@SimonGuilloud
issue with leftForall
cf2710b
@SimonGuilloud
Improvements to TPTP import and Eequivalence Checker for forall(x, tr…
48f2510 
…ue) and forall(x, false).
@SimonGuilloud
update proofparser to understand skolemization level 2 steps
12ceb95
@SimonGuilloud
update prover9 integration to support skolemization, fixes.
f19566f
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