scientific article

zbMath1165.03011MaRDI QIDQ3543581

Andrzej Szałas, Renate A. Schmidt, Dov M. Gabbay

Publication date: 4 December 2008

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

modal logicquantifier eliminationresolutionclassical logicsecond-order theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (27)

Symbol elimination and applications to parametric entailment problems ⋮ Semantic forgetting in expressive description logics ⋮ Converse-PDL with regular inclusion axioms: a framework for MAS logics ⋮ Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications ⋮ Knowledge forgetting in propositional \(\mu\)-calculus ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Dual forgetting operators in the context of weakest sufficient and strongest necessary conditions ⋮ The Ackermann approach for modal logic, correspondence theory and second-order reduction ⋮ Discrete dualities for \(n\)-potent MTL-algebras and 2-potent BL-algebras ⋮ Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA ⋮ Projection and scope-determined circumscription ⋮ Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey ⋮ On the limits of forgetting in answer set programming ⋮ Stratified guarded first-order transition systems ⋮ Second-order quantifier elimination in higher-order contexts with applications to the semantical analysis of conditionals ⋮ First-Order Resolution Methods for Modal Logics ⋮ Annotation theories over finite graphs ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ A fixed-point theorem for Horn formula equations ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ On syntactic forgetting under uniform equivalence ⋮ FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions ⋮ Towards incorporating background theories into quantifier elimination ⋮ Completeness and Correspondence in Hybrid Logic via an Extension of SQEMA ⋮ Forgetting in multi-agent modal logics ⋮ A new methodology for developing deduction methods ⋮ Voting by eliminating quantifiers

This page was built for publication: