SPASS+T
From MaRDI portal
Cited in
(25)- Solving quantified verification conditions using satisfiability modulo theories
- Layered clause selection for theory reasoning (short paper)
- Checkfence
- Monotonox
- On automation in the verification of software barriers: experience report
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Jahob
- Beagle
- SMTtoTPTP
- Proving infinite satisfiability
- A heuristic prover for real inequalities
- A heuristic prover for real inequalities
- The TPTP typed first-order form with arithmetic
- 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
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- An instantiation scheme for satisfiability modulo theories
- Theorem proving in large formal mathematics as an emerging AI field
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- MetiTarski: An Automatic Prover for the Elementary Functions
- MetiTarski: An automatic theorem prover for real-valued special functions
This page was built for software: SPASS+T
