Practically useful variants of definitional translations to normal form
From MaRDI portal
Recommendations
- On the practical value of different definitional translations to normal form
- On different structure-preserving translations to normal form
- Translation of resolution proofs into short first-order proofs without choice axioms.
- scientific article; zbMATH DE number 994053
- An optimality result for clause form translation
Cites work
- A note on assumptions about Skolem functions
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- A structure-preserving clause form translation
- Controlled integration of the cut rule into connection tableau calculi
- scientific article; zbMATH DE number 48763 (Why is no real title available?)
- scientific article; zbMATH DE number 534879 (Why is no real title available?)
- Minimizing the number of clauses by renaming
- On different structure-preserving translations to normal form
- On the practical value of different definitional translations to normal form
- The TPTP problem library
- Theorem Proving via General Matings
Cited in
(5)- scientific article; zbMATH DE number 994053 (Why is no real title available?)
- scientific article; zbMATH DE number 67125 (Why is no real title available?)
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- On the practical value of different definitional translations to normal form
- On different structure-preserving translations to normal form
This page was built for publication: Practically useful variants of definitional translations to normal form
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1854384)
