SPASS+T
From MaRDI portal
Software:16784
swMATH4613MaRDI QIDQ16784FDOQ16784
Author name not available (Why is that?)
Cited In (20)
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Beagle – A Hierarchic Superposition Theorem Prover
- A heuristic prover for real inequalities
- An instantiation scheme for satisfiability modulo theories
- Layered clause selection for theory reasoning (short paper)
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- MetiTarski: An automatic theorem prover for real-valued special functions
- Solving quantified verification conditions using satisfiability modulo theories
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- On automation in the verification of software barriers: experience report
- Proving Infinite Satisfiability
- MetiTarski: An Automatic Prover for the Elementary Functions
- Extensional Crisis and Proving Identity
- The TPTP Typed First-Order Form with Arithmetic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- A Heuristic Prover for Real Inequalities
- Automated Reasoning for Hybrid Systems — Two Case Studies —
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
This page was built for software: SPASS+T
