Deontic Defeasible Description Logic (3DL)
Defeasible ALC with normative obligations, permissions, and independent expectation/ideality rankings; minimal entailment is EXPTIME-complete.
Deontic Description LogicsThe directory29 published entries
Welcome to LogicalZoo
Explore formal logics, their expressive power, and their relationships. A growing reference guide from syntax and semantics to decidability and complexity.
Find a logic
All logics
29 entriesAttributive Concept Language with Complements
A foundational description logic with Boolean concept constructors and existential and universal role restrictions.
Description LogicsBrouwer Modal Logic B
Normal propositional modal logic B, with reflexive and symmetric Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsComputation Tree Logic
A branching-time temporal logic that combines path quantification with temporal operators.
Temporal LogicsThe Modal Logic Cube
An atlas of the 15 distinct classical normal propositional modal logics generated from K by D, T, B, 4 and 5.
Normal Modal LogicsDyadic Deontic Logic (Conditional Obligation)
A family of conditional obligation logics with primitive O(consequent | condition), often interpreted by optimal condition-worlds.
Deontic LogicsDescription Logic Programs (DLP)
An expressive intersection of description logics and Horn logic programming, permitting rule–ontology translations without arbitrary disjunctive/existential heads.
Description Logics and Rule SystemsFirst-Order Logic
Classical predicate logic with quantification over individuals, relational structures, and Tarskian semantics.
Classical LogicsTwo-Variable First-Order Logic
The two-variable fragment of relational first-order logic, allowing only two reusable variable symbols. Satisfiability is NEXPTIME-complete.
Fragments of First-Order LogicGuarded Fragment
A fragment of relational first-order logic whose quantifiers are guarded by atomic formulas. Satisfiability is 2EXPTIME-complete.
Fragments of First-Order LogicClassical Higher-Order Logic
Classical simple type theory with quantification over individuals, predicates, and functions. Standard and Henkin semantics differ in their function domains.
Higher-Order LogicsBasic Normal Modal Logic K
Normal propositional modal logic K, with arbitrary Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsTransitive Modal Logic K4
Normal propositional modal logic K4, with transitive Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsTransitive Euclidean Modal Logic K45
Normal propositional modal logic K45, with transitive and Euclidean Kripke accessibility; local satisfiability is NP-complete.
Normal Modal LogicsEuclidean Modal Logic K5
Normal propositional modal logic K5, with Euclidean Kripke accessibility; local satisfiability is NP-complete.
Normal Modal LogicsNormal Modal Logic KB
Normal propositional modal logic KB, with symmetric Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsSymmetric Euclidean Modal Logic KB5
Normal propositional modal logic KB5, with symmetric and Euclidean Kripke accessibility; local satisfiability is NP-complete.
Normal Modal LogicsNormal Modal Logic KD
Normal propositional modal logic KD, with serial Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsSerial Transitive Modal Logic KD4
Normal propositional modal logic KD4, with serial and transitive Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsSerial Transitive Euclidean Modal Logic KD45
Normal propositional modal logic KD45, with serial and transitive and Euclidean Kripke accessibility; local satisfiability is NP-complete.
Normal Modal LogicsSerial Euclidean Modal Logic KD5
Normal propositional modal logic KD5, with serial and Euclidean Kripke accessibility; local satisfiability is NP-complete.
Normal Modal LogicsNormal Modal Logic KDB
Normal propositional modal logic KDB, with serial and symmetric Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsNormal Modal Logic T
Normal propositional modal logic KT, with reflexive Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsLinear Temporal Logic
Linear Temporal Logic (LTL) is a propositional temporal logic for expressing properties of infinite execution traces using next, until, eventually, and always. It is widely used to specify and verify reactive systems.
Temporal LogicsClassical Propositional Logic
The logic of truth-functional combinations of propositions, forming a foundation for classical inference and the SAT problem.
Classical LogicsNormal Modal Logic S4
Normal propositional modal logic S4, with reflexive and transitive Kripke accessibility; local satisfiability is PSPACE-complete.
Normal Modal LogicsNormal Modal Logic S5
Normal propositional modal logic S5, with reflexive and Euclidean Kripke accessibility; local satisfiability is NP-complete.
Normal Modal LogicsStandard Deontic Logic (SDL)
Normal deontic logic KD: monadic obligation over serial Kripke frames, with permission defined by duality.
Deontic LogicsSROIQ: An Expressive Description Logic
Expressive description logic supporting nominals, inverse roles, qualified number restrictions, and regular complex role inclusions; basis of OWL 2 DL.
Description Logics