The following pages link to Spartacus (Q24354):
Displaying 14 items.
- Symmetric blocking (Q897931) (← links)
- An assumption-based approach for solving the minimal S5-satisfiability problem (Q1799062) (← links)
- A prover dealing with nominals, binders, transitivity and relation hierarchies (Q2303237) (← links)
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments (Q2303247) (← links)
- A goal-directed decision procedure for hybrid PDL (Q2351150) (← links)
- : A Resolution-Based Prover for Multimodal K (Q2817940) (← links)
- An efficient approach to nominal equalities in hybrid logic tableaux (Q2901189) (← links)
- Completeness and termination for a Seligman-style tableau system (Q2987043) (← links)
- Hybrid Specification of Reactive Systems: An Institutional Approach (Q3095244) (← links)
- InKreSAT: Modal Reasoning via Incremental Reduction to SAT (Q4928458) (← links)
- Modal Logic S5 Satisfiability in Answer Set Programming (Q5019595) (← links)
- Terminating Tableaux for Hybrid Logic with Eventualities (Q5747764) (← links)
- Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic (Q5747765) (← links)
- Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies (Q5892513) (← links)
