kframework matching-logic-prover issues

kframework / matching-logic-prover

15 stars 4 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Add a sample proof for one rewriting step

#85 zhengyao-lin opened 4 years ago
0
Support for Coq's tactic syntax (`.`, `;`)

#84 h0nzZik opened 4 years ago
0
Delete the rest of the prover (in the notation branch).

#83 h0nzZik opened 4 years ago
0
Syntactic matching for the `apply` strategy.

#82 h0nzZik opened 4 years ago
0
Notations and disambiguation

#81 h0nzZik closed 4 years ago
0
Symbols in prelude

#80 h0nzZik closed 4 years ago
1
Fix parsing timestamps being too permissive

#79 nishantjr closed 4 years ago
1
Generalize matching

#78 lucaspena opened 4 years ago
0
Move to LLVM backend

#77 nishantjr closed 4 years ago
0
Smt hooks

#76 h0nzZik closed 4 years ago
1
Merge symbolic unit tests and unit-test semantics

#75 nishantjr opened 4 years ago
0
matching over heap variables

#74 lucaspena closed 4 years ago
0
smt prelude in file

#73 h0nzZik closed 4 years ago
1
Port extensions to #match from the OOPSLA branch

#72 lucaspena opened 4 years ago
0
Deterministic choice operator

#71 h0nzZik opened 4 years ago
0
add *.expected

#70 h0nzZik closed 4 years ago
0
Another Hyperproperties stuff

#69 h0nzZik closed 4 years ago
2
strategies are now in the <k> cell. goals in <claim>

#68 nishantjr closed 4 years ago
0
Fix Kore driver

#67 h0nzZik closed 4 years ago
2
Preparation for Hyperproperties - part 2 (strategies)

#66 h0nzZik closed 4 years ago
0
Preparation for Hyperproperties - part 1

#65 h0nzZik closed 4 years ago
0
Preparation for Hyperproperties

#64 h0nzZik closed 4 years ago
1
Deterministic choice operators

#63 nishantjr opened 4 years ago
1
Testing infrastructure tweaks

#62 nishantjr closed 4 years ago
0
Various fixes

#61 h0nzZik closed 4 years ago
0
`\typeof` construct, set variables

#60 h0nzZik closed 4 years ago
4
Use a list of <goal>s instead of a set

#59 nishantjr closed 4 years ago
1
Shape analysis

#58 lucaspena opened 4 years ago
2
Remove Global Environment.

#57 nishantjr opened 4 years ago
0
Remove non-capture free substitution and add unit tests

#56 nishantjr closed 4 years ago
0
Clean up Metamath Definition

#55 xc93 closed 4 years ago
0
Unit tests

#54 nishantjr closed 4 years ago
0
Update K

#53 nishantjr closed 4 years ago
0
Axiom names are duplicated

#52 nishantjr opened 4 years ago
0
Strategies `apply` and `inst-exists`

#51 h0nzZik closed 4 years ago
0
Preparation for AML/Unsorting

#50 h0nzZik closed 4 years ago
0
Replace `\hole()` with `#hole`

#49 h0nzZik opened 4 years ago
4
Matchig variables - duplicated rule

#48 h0nzZik opened 4 years ago
0
apply-equation should check functionality of terms in substitution

#47 h0nzZik opened 4 years ago
0
replace-svar-with-constant

#46 h0nzZik opened 4 years ago
0
Remove the ability to have unnamed axioms.

#45 h0nzZik opened 4 years ago
0
`match` strategy working with axioms and arbitrary formulas

#44 h0nzZik opened 4 years ago
0
Prettyprint/produce proof tree

#43 nishantjr opened 4 years ago
2
`intros` non-predicate patterns

#42 h0nzZik closed 4 years ago
2
isFOLPattern

#41 h0nzZik opened 4 years ago
0
Transition to AML: sorts

#40 h0nzZik opened 4 years ago
18
Strategy: `duplicate` and various fixes

#39 h0nzZik closed 4 years ago
0
Coq lang

#38 lucaspena opened 4 years ago
0
strategy: `instantiate-universals`

#37 h0nzZik closed 4 years ago
5
Local contexts, intros, replace-evar-with-func-constant

#36 h0nzZik closed 4 years ago
0