KoMeT

swMATH28720MaRDI QIDQ40434FDOQ40434

Author name not available (Why is that?)

Described by source

• On the practical value of different definitional translations to normal form

Cited In (12)

• Specifying and Verifying Organizational Security Properties in First-Order Logic
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• A uniform procedure for converting matrix proofs into sequent-style systems
• IeanCOP: lean connection-based theorem proving
• ILF-SETHEO
• Practically useful variants of definitional translations to normal form
• Prolog technology for default reasoning: proof theory and compilation techniques
• A solver for QBFs in negation normal form
• Integration of automated and interactive theorem proving in ILF
• T-string unification: Unifying prefixes in non-classical proof methods
• 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