Pages that link to "Item:Q1663240"
From MaRDI portal
The following pages link to Hammer for Coq: automation for dependent type theory (Q1663240):
Displaying 21 items.
- CoqHammer (Q41110) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- A Knuth-Bendix-like ordering for orienting combinator equations (Q2096451) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Relaxed weighted path order in theorem proving (Q2209265) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Restricted combinatory unification (Q2305407) (← links)
- Portfolio theorem proving and prover runtime prediction for geometry (Q2631959) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) (Q5049022) (← links)
- (Q5109521) (← links)
- (Q5111310) (← links)
- (Q5875421) (← links)
- (Q5875422) (← links)
- Superposition with lambdas (Q5918381) (← links)
- Making higher-order superposition work (Q5918403) (← links)
- Making higher-order superposition work (Q5918575) (← links)
- Superposition with lambdas (Q5919500) (← links)
- An automatically verified prototype of the Android permissions system (Q6103592) (← links)