issues
search
Formal-Systems-Laboratory
/
matching-logic-mm0
Formalisation of Matching Logic in Metamath 0
BSD 3-Clause "New" or "Revised" License
0
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Theory separation
#29
MirceaS
opened
2 months ago
0
Alphabet generalisation
#28
MirceaS
opened
1 year ago
1
put mm0/mm1 files inside their own directory and only compile those files from there
#27
MirceaS
opened
1 year ago
0
Cong of equiv optimizations
#26
MirceaS
closed
1 year ago
0
Assumptions removal
#25
MirceaS
closed
1 year ago
1
More proofs relating to `top-implies-fp`.
#24
nishantjr
closed
1 year ago
1
Replace incorrect/unsound assumption for `der_equality`
#23
nishantjr
closed
1 year ago
0
Renamed theorems and proved some more of the assumptions
#22
MirceaS
closed
1 year ago
0
Fixes and utils
#21
MirceaS
closed
1 year ago
0
AppCtx axioms missing freshness constraints
#20
MirceaS
closed
1 year ago
1
Prove `top-implies-fp-init`, bug fixes, property based testing using Hypothesis.
#19
nishantjr
closed
1 year ago
1
Prove alpha renaming for exists and mu
#18
MirceaS
opened
1 year ago
0
Prove assumptions: `top_implies_fp_*`
#17
nishantjr
opened
1 year ago
0
Freshness axioms & prove top-implies-fp
#16
nishantjr
closed
1 year ago
0
Benchmark: Use CPU time rather than wall clock time
#15
MirceaS
opened
1 year ago
1
Organize the 24-derivatives file.
#14
nishantjr
closed
1 year ago
2
Refactorings & Benchmarks
#13
nishantjr
closed
1 year ago
1
Prove `fp-implies-top`
#12
nishantjr
closed
1 year ago
0
Remove positivity hack
#11
nishantjr
closed
1 year ago
0
Update maude version
#10
nishantjr
closed
1 year ago
0
Test using `mm0-c`
#9
nishantjr
closed
1 year ago
0
DRAFT PR: Top implies fp
#8
MirceaS
closed
1 year ago
1
Cleanup + code organization
#7
MirceaS
opened
1 year ago
1
lisp code test theorems
#6
MirceaS
opened
1 year ago
1
Prove `der_equality`
#5
nishantjr
closed
1 year ago
2
Axioms: Relax disjointness criteria for singleton
#4
nishantjr
closed
1 year ago
2
Proofs2
#3
MirceaS
closed
1 year ago
0
Normalization and application contexts
#2
nishantjr
closed
1 year ago
0
Normalization and application contexts
#1
nishantjr
closed
1 year ago
0