Cited in
(17)- Towards a notion of unsatisfiable and unrealizable cores for LTL
- T-string unification: unifying prefixes in non-classical proof methods
- SETHEO
- SCOTT
- linTAP
- METEOR
- ILF-SETHEO
- A uniform procedure for converting matrix proofs into sequent-style systems
- IeanCOP: lean connection-based theorem proving
- Practically useful variants of definitional translations to normal form
- ILF-SETHEO
- Prolog technology for default reasoning: proof theory and compilation techniques
- Specifying and verifying organizational security properties in first-order logic
- A solver for QBFs in negation normal form
- Integration of automated and interactive theorem proving in ILF
- Converting non-classical matrix proofs into sequent-style systems
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
This page was built for software: KoMeT
