SPASS
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Labelled splitting
- Automated verification of refinement laws
- Solving quantified verification conditions using satisfiability modulo theories
- A new methodology for developing deduction methods
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Cocktail
- LEO-II
- PyRes
- Nitpick
- SETHEO
- Shellcheck
- CoLiS
- SOLAR
- Limited resource strategy in resolution theorem proving
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- AutoBayes/CC
- PLAGIATOR
- TGTP
- MizarMode
- SafeGen
- CASL
- TAPS
- MPTP
- MPTP 0.2
- OTTER
- VAMPIRE
- KARO
- Deciding the E^+-class by an a posteriori, liftable order
- THF0
- MAYA
- Evaluating general purpose automated theorem proving systems
- SAT-based decision procedures for classical modal logics
- Using resolution for testing modal satisfiability and building models
- A formally verified interpreter for a shell-like programming language
- TPTP
- Darwin
- Metis
- Formalization of the resolution calculus for first-order logic
- A deontic logic reasoning infrastructure
- SPASS+T
- MoMM
- Superposition with structural induction
- On combining algebraic specifications with first-order logic via Athena
- cvc3
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Prover9
- An assumption-based approach for solving the minimal S5-satisfiability problem
- Superposition for -free higher-order logic
- A generic framework for implicate generation modulo theories
- Efficient encodings of first-order Horn formulas in equational logic
- A resolution-based calculus for preferential logics
- Automated deduction techniques for the management of personalized documents
- FINDER
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- TSPASS
- Deciding the guarded fragments by resolution
- SATCHMO
- DCTP
- SCOTT
- Satallax
- E-Darvin
- Mace4
- MML
- AURA
- Hets
- Sledgehammer
- E-SETHEO
- ESC4
- TATL
- CVC Lite
- LoTREC
- Knowledge-based proof planning
- Cadence SMV
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- Ralf
- ARA
- RALL
- Improving ENIGMA-style clause selection while learning from history
- Handling transitive relations in first-order automated reasoning
- MBase
- StarExec
- Subsumption demodulation in first-order theorem proving
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Local is best: efficient reductions to modal logic \textsf{K}
- Theorem proving as constraint solving with coherent logic
- An efficient subsumption test pipeline for BS(LRA) clauses
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
- SCL(EQ): SCL for first-order logic with equality
- Local reductions for the modal cube
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- CERES
- Herod
- Pilate
- iProver-Eq
- CVC4
- TLAPS
- iProver
This page was built for software: SPASS
