Spartacus
From MaRDI portal
Cited in
(25)- An assumption-based approach for solving the minimal S5-satisfiability problem
- Herod
- Pilate
- FaCT++
- A prover dealing with nominals, binders, transitivity and relation hierarchies
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- A goal-directed decision procedure for hybrid PDL
- Sibyl
- HTab
- HyLoTab
- \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
- An efficient approach to nominal equalities in hybrid logic tableaux
- HyLoRes
- Completeness and termination for a Seligman-style tableau system
- Hybrid specification of reactive systems: an institutional approach
- InKreSAT
- HGen
- BDDTab
- InKreSAT: modal reasoning via incremental reduction to SAT
- Modal logic S5 satisfiability in answer set programming
- Terminating Tableaux for Hybrid Logic with Eventualities
- Herod and Pilate: two tableau provers for basic hybrid logic
- Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
- MOIN
- Symmetric blocking
This page was built for software: Spartacus
