Ivy

swMATH10279MaRDI QIDQ22242FDOQ22242

Author name not available (Why is that?)

Cited In (40)

• A decidable and expressive fragment of Many-Sorted first-order linear temporal logic
• Automated Reasoning
• Sound verification procedures for temporal properties of infinite-state systems
• Computer Solutions of Problems in Inverse Semigroups
• Understanding Resolution Proofs through Herbrand’s Theorem
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Automated Deduction – CADE-19
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Title not available (Why is that?)
• ATP Cross-Verification of the Mizar MPTP Challenge Problems
• Title not available (Why is that?)
• Integrating external deduction tools with ACL2
• Title not available (Why is that?)
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• PRocH: Proof Reconstruction for HOL Light
• Automated proof construction in type theory using resolution
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Translation of resolution proofs into short first-order proofs without choice axioms
• Bounded Quantifier Instantiation for Checking Inductive Invariants
• Temporal prophecy for proving temporal properties of infinite-state systems
• Pollack-inconsistency
• Formal proofs about rewriting using ACL2
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Learning inductive invariants by sampling from frequency distributions
• Extending Sledgehammer with SMT solvers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Title not available (Why is that?)
• More SPASS with Isabelle
• Hammering towards QED
• Title not available (Why is that?)
• SGGS decision procedures
• Title not available (Why is that?)
• Towards Self-verification of HOL Light

This page was built for software: Ivy