Normal form transformations
This is a detailed overview about normal forms in logic and their transformations. There are various applications of normal forms, like in automated deduction, the reduction of the original inference problem to simple calculi like resolution and paramodulation, and, in general, for the appropriate application of heuristics.NEWLINENEWLINENEWLINEFor example, when working in clausal forms, the whole logical structure of the original formulae is stored in atom formulae, and terms, quantifiers and the logical operators are essentially removed. Many normal form transformations are equivalence-preserving, others, like Skolem normal form, extend the signature of the formula and are not equivalence-preserving. Rather, Skolem normal form preserves satisfiability or validity-equivalence, in the respective application. Also, normal forms in nonclassical logics are considered.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
- The problem of \(\Pi_{2}\)-cut-introduction
- Bounded treewidth as a key to tractability of knowledge representation and reasoning
- Reasoning in description logics by a reduction to disjunctive datalog
- Translation of resolution proofs into short first-order proofs without choice axioms
- A note on the size of prenex normal forms
- On Stronger Calculi for QBFs
- Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination
- Combinations of Theories for Decidable Fragments of First-Order Logic
- scientific article; zbMATH DE number 67125 (Why is no real title available?)
- Canonical signed calculi with multi-ary quantifiers
- Combining decision procedures by (model-)equality propagation
- Role of normal logical form in decision-making and knowledge management
- Proof Transformations and Structural Invariance
- Scalable fine-grained proofs for formula processing
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
- Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)
- Finding connections via satisfiability solving
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- Unification and anti-unification in applicative matching logic
- Semantic forgetting in expressive description logics
- Quantifier simplification by unification in SMT
- Deciding expressive description logics in the framework of resolution
This page was built for publication: Normal form transformations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751356)
