SPASS+T
From MaRDI portal
Cited in
(25)- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- A heuristic prover for real inequalities
- Extending a Resolution Prover for Inequalities on Elementary Functions
- A heuristic prover for real inequalities
- An instantiation scheme for satisfiability modulo theories
- Extensional crisis and proving identity
- Proving infinite satisfiability
- 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
- The TPTP typed first-order form with arithmetic
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Checkfence
- Monotonox
- Jahob
- Beagle
- SMTtoTPTP
- On automation in the verification of software barriers: experience report
- Theorem proving in large formal mathematics as an emerging AI field
- MetiTarski: An Automatic Prover for the Elementary Functions
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Beagle -- a hierarchic superposition theorem prover
- 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
