The following pages link to Ivy (Q22242):
Displaying 40 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- A decidable and expressive fragment of Many-Sorted first-order linear temporal logic (Q821564) (← links)
- Sound verification procedures for temporal properties of infinite-state systems (Q832273) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- Formal proofs about rewriting using ACL2 (Q1610218) (← links)
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms (Q1696580) (← links)
- Automated proof construction in type theory using resolution (Q1868508) (← links)
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420) (← links)
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning (Q2055851) (← links)
- Temporal prophecy for proving temporal properties of infinite-state systems (Q2058382) (← links)
- SGGS decision procedures (Q2096457) (← links)
- Learning inductive invariants by sampling from frequency distributions (Q2225478) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Translation of resolution proofs into short first-order proofs without choice axioms (Q2486578) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- (Q2723415) (← links)
- Understanding Resolution Proofs through Herbrand’s Theorem (Q2851942) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors (Q2961566) (← links)
- Bounded Quantifier Instantiation for Checking Inductive Invariants (Q3303891) (← links)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs (Q3498463) (← links)
- ATP Cross-Verification of the Mizar MPTP Challenge Problems (Q3498492) (← links)
- Computer Solutions of Problems in Inverse Semigroups (Q3562322) (← links)
- Using the TPTP Language for Writing Derivations and Finite Interpretations (Q3613401) (← links)
- Towards Self-verification of HOL Light (Q3613408) (← links)
- (Q4411849) (← links)
- (Q4471941) (← links)
- (Q4471942) (← links)
- (Q4551175) (← links)
- PRocH: Proof Reconstruction for HOL Light (Q4928443) (← links)
- (Q5009435) (← links)
- (Q5079756) (← links)
- Pollack-inconsistency (Q5170237) (← links)
- Hammering towards QED (Q5195271) (← links)
- (Q5219924) (← links)
- Automated Reasoning (Q5307058) (← links)
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker (Q5883751) (← links)
- Automated Deduction – CADE-19 (Q5900728) (← links)
