Ivy
From MaRDI portal
Cited in
(71)- Integrating external deduction tools with ACL2
- ACL2
- Minha
- RegStab
- AutoBayes/CC
- RESTART
- Formal proofs about rewriting using ACL2
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- Automated proof construction in type theory using resolution
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- Temporal prophecy for proving temporal properties of infinite-state systems
- TRX
- SGGS decision procedures
- CERES
- TLAPS
- TLC
- Milawa
- Gandalf
- Learning inductive invariants by sampling from frequency distributions
- SystemOnTPTP
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Translation of resolution proofs into short first-order proofs without choice axioms
- MODIST
- Cubicle
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- scientific article; zbMATH DE number 1614692 (Why is no real title available?)
- VeriCon
- Understanding Resolution Proofs through Herbrand’s Theorem
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- More SPASS with Isabelle
- PSync
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- HOL90
- OMEGA
- Bounded quantifier instantiation for checking inductive invariants
- ByMC
- Verdi
- ProofTool
- DynamoDB
- Chapar
- FastTrack
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- Computer solutions of problems in inverse semigroups.
- Using the TPTP Language for Writing Derivations and Finite Interpretations
- Towards Self-verification of HOL Light
- GeoNames
- FLOTTER
- scientific article; zbMATH DE number 1948188 (Why is no real title available?)
- scientific article; zbMATH DE number 2079834 (Why is no real title available?)
- scientific article; zbMATH DE number 2079835 (Why is no real title available?)
- scientific article; zbMATH DE number 1796151 (Why is no real title available?)
- PRocH: proof reconstruction for HOL Light
- Synchronizing the asynchronous
- A decidable fragment of second order logic with applications to synthesis
- Pollack-inconsistency
- Hammering towards QED
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Automated Reasoning
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Translation of resolution proofs into short first-order proofs without choice axioms.
- Koala
- Ivy
- IronFleet
- dBug
- DCatch
- A decidable and expressive fragment of many-sorted first-order linear temporal logic
- Sound verification procedures for temporal properties of infinite-state systems
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
This page was built for software: Ivy
