SPASS
From MaRDI portal
Software:16295
swMATH4108MaRDI QIDQ16295FDOQ16295
Author name not available (Why is that?)
Official website: http://www.spass-prover.org/
Cited In (only showing first 100 items - show all)
- Herbrand constructivization for automated intuitionistic theorem proving
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Automatic construction and verification of isotopy invariants
- Computing Tiny Clause Normal Forms
- Title not available (Why is that?)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Superposition and Model Evolution Combined
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- The higher-order prover \textsc{Leo}-II
- Semantically-guided goal-sensitive reasoning: model representation
- Semi-intelligible Isar proofs from machine-generated proofs
- Model-theoretic methods in combined constraint satisfiability
- New results on rewrite-based satisfiability procedures
- Mathematical Knowledge Management
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Mining the Archive of Formal Proofs
- A combined superposition and model evolution calculus
- Automated inference of finite unsatisfiability
- CTL-RP: A computation tree logic resolution prover
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- Using tableau to decide description logics with full role negation and identity
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Computer supported mathematics with \(\Omega\)MEGA
- Title not available (Why is that?)
- Solving quantified verification conditions using satisfiability modulo theories
- Automated verification of refinement laws
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- An empirical analysis of modal theorem provers
- LEO-II
- MizarMode
- CASL
- MPTP 0.2
- MAYA
- MoMM
- SPASS+T
- Evaluating general purpose automated theorem proving systems
- Title not available (Why is that?)
- CERES
- Herod
- iProver-Eq
- Pilate
- CalcCheck
- Equinox
- iProver
- TeMP
- HyLoTab
- Sledgehammer: judgement day
- OMEGA
- CLIN
- DISCOUNT
- Lambda-Clam
- LOUI
- Denali
- GAPT
- ProofTool
- Peers-mcd
- Scavenger
- leanK
- Twee
- FLOTTER
- PARIS
- Network Security Policy Verification
- Theorem proving in large formal mathematics as an emerging AI field
- Sqrt_Babylonian
- WhaleProver
- Model evolution with equality -- revised and implemented
- Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans
- Statically safe program generation with SafeGen
- Adimen-SUMO
- CLProver
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Title not available (Why is that?)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Case splitting in an automatic theorem prover for real-valued special functions
- SAD as a mathematical assistant -- how should we go from here to there?
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- On interpolation in automated theorem proving
- Premise selection for mathematics by corpus analysis and kernel methods
- The model evolution calculus as a first-order DPLL method
- One logic to use them all
- Automated verification of relational while-programs
- Labelled splitting
- More SPASS with Isabelle
- The TPTP World -- infrastructure for automated reasoning
- System Description: Spass Version 3.0
- Metis
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- SPASS \& FLOTTER version 0.42
- Splitting through new proposition symbols
- Automated Reasoning
- Scalable fine-grained proofs for formula processing
- Superposition with lambdas
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Vampire with a brain is a good ITP hammer
- Automated Deduction – CADE-20
- An interactive derivation viewer
- Simulation and synthesis of deduction calculi
- Title not available (Why is that?)
This page was built for software: SPASS