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