diff --git a/pddl/_validation.py b/pddl/_validation.py
index 63ee71c3..dcad57b5 100644
--- a/pddl/_validation.py
+++ b/pddl/_validation.py
@@ -19,7 +19,7 @@
 from pddl.action import Action
 from pddl.custom_types import name as name_type
 from pddl.custom_types import namelike, to_names, to_types  # noqa: F401
-from pddl.definitions.base import TypesDef
+from pddl.definitions.types_def import TypesDef
 from pddl.exceptions import PDDLValidationError
 from pddl.helpers.base import check, ensure_set
 from pddl.logic import Predicate
diff --git a/pddl/validation/__init__.py b/pddl/builders/__init__.py
similarity index 80%
rename from pddl/validation/__init__.py
rename to pddl/builders/__init__.py
index 43f3674e..dffaf073 100644
--- a/pddl/validation/__init__.py
+++ b/pddl/builders/__init__.py
@@ -10,4 +10,4 @@
 # https://opensource.org/licenses/MIT.
 #
 
-"""This package includes validation functions of PDDL domains/problems."""
+"""This package includes builder classes for PDDL domains and problems."""
diff --git a/pddl/builders/base.py b/pddl/builders/base.py
new file mode 100644
index 00000000..d46621cb
--- /dev/null
+++ b/pddl/builders/base.py
@@ -0,0 +1,171 @@
+#
+# Copyright 2021-2023 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pddl.
+#
+# Use of this source code is governed by an MIT-style
+# license that can be found in the LICENSE file or at
+# https://opensource.org/licenses/MIT.
+#
+
+"""This module includes the base classes for the PDDL builders."""
+
+from abc import ABC, abstractmethod
+from typing import AbstractSet, Generic, Type, TypeVar, Set, Optional, Dict, Callable
+
+from pddl.builders.types_def import TypesDef, MutableTypesDef
+from pddl.core import Domain, Problem
+from pddl.custom_types import namelike
+from pddl.exceptions import PDDLValidationError
+from pddl.helpers.base import assert_
+from pddl.logic.terms import Term
+from pddl.requirements import Requirements
+
+T = TypeVar("T", Domain, Problem)
+
+
+class BaseBuilder(ABC, Generic[T]):
+    """A base class for the PDDL builders."""
+
+    @abstractmethod
+    def build(self) -> T:
+        """Build the PDDL object."""
+
+
+class _NoDuplicateList(list):
+    """A list that does not allow duplicates."""
+
+    def __init__(
+        self, item_name: str, exception_cls: Type[Exception] = PDDLValidationError
+    ) -> None:
+        """Initialize the list."""
+        super().__init__()
+        self.__item_name = item_name
+        self.__exception_cls = exception_cls
+        # this is for O(1) lookup
+        self.__elements = set()
+
+    def append(self, item) -> None:
+        """Append an item to the list."""
+        if item in self.__elements:
+            raise PDDLValidationError(f"duplicate {self.__item_name}: '{item}'")
+        super().append(item)
+        self.__elements.add(item)
+
+    def extend(self, iterable) -> None:
+        """Extend the list with an iterable."""
+        for item in iterable:
+            self.append(item)
+
+    def __contains__(self, item):
+        """Check if the list contains an item."""
+        return item in self.__elements
+
+    def get_set(self) -> AbstractSet:
+        """Get the set of elements."""
+        return self.__elements
+
+
+class _Context:
+    """A context for the PDDL builders."""
+
+    def __init__(self) -> None:
+        """Initialize the context."""
+        self.__requirements: _NoDuplicateList = _NoDuplicateList("requirement")
+        self.__types_def: MutableTypesDef = MutableTypesDef()
+
+        self.__used_names: Dict[namelike, object] = {}
+
+    @property
+    def requirements(self) -> AbstractSet[Requirements]:
+        """Get the requirements."""
+        return self.__requirements.get_set()
+
+    @property
+    def has_typing(self) -> bool:
+        """Check if the typing requirement is specified."""
+        return Requirements.TYPING in self.requirements
+
+    @property
+    def types_def(self) -> MutableTypesDef:
+        """Get the types definition."""
+        return self.__types_def
+
+    def add_requirement(self, requirement: Requirements) -> None:
+        """Add a requirement to the domain."""
+        self.__requirements.append(requirement)
+
+    def add_type(
+        self, child_type: namelike, parent_type: Optional[namelike] = None
+    ) -> None:
+        """Add a type to the domain."""
+        self.check_name_not_already_used(child_type, "type")
+        self.check_name_not_already_used(parent_type, "type") if parent_type is not None else None
+        self.check_typing_requirement_for_types(child_type, parent_type)
+
+        self.__types_def.add_type(child_type, parent_type)
+
+        self.add_used_name(child_type, "type")
+        self.add_used_name(parent_type, "type") if parent_type is not None else None
+
+    def add_used_name(self, name: namelike, obj: object) -> None:
+        """Add a name to the used names."""
+        self.__used_names[name] = obj
+
+    def get_used_name(self, name: namelike) -> Optional[object]:
+        """Add a name to the used names."""
+        return self.__used_names.get(name)
+
+    def check_typing_requirement_for_types(
+        self, child_type: namelike, parent_type: Optional[namelike] = None
+    ) -> None:
+        """Check that the typing requirement is specified."""
+        if not self.has_typing:
+            raise PDDLValidationError(
+                f"typing requirement is not specified, but the following types were used: {child_type}"
+                + (f" -> {parent_type}" if parent_type else "")
+            )
+
+    def check_name_not_already_used(self, new_name: namelike, new_object: object) -> None:
+        """Check that the name is not already used."""
+        if new_name in self.__used_names:
+            raise PDDLValidationError(
+                f"name '{new_name}' of object '{new_object}' is already used for '{self.__used_names[new_name]}'"
+            )
+
+    def check_types_are_available(self, term: Term) -> None:
+        """Check that the types of a term are available in the domain."""
+        if not self.types_def.are_types_available(term.type_tags):
+            raise PDDLValidationError(
+                f"types {sorted(term.type_tags)} of term '{term}' are not in available types {self.types_def.sorted_all_types}"
+            )
+
+
+class _Definition:
+    """Abstract class for a PDDL definition."""
+
+    def __init__(
+        self, context: _Context
+    ) -> None:
+        """Initialize the PDDL definition."""
+        assert_(type(self) is not _Definition)
+        self.__context = context
+
+    @property
+    def _context(self) -> _Context:
+        """Get the context."""
+        return self.__context
+
+    @property
+    def has_typing(self) -> bool:
+        """Check if the typing requirement is specified."""
+        return self.__context.has_typing
+
+    def _check_typing_requirement_for_term(self, term: Term) -> None:
+        """Check that the typing requirement is specified for a term."""
+        if not self.has_typing and len(term.type_tags) > 0:
+            raise PDDLValidationError(
+                f"typing requirement is not specified, but the following types for term '{term}' were used: {term.type_tags}"
+            )
diff --git a/pddl/builders/constants_def.py b/pddl/builders/constants_def.py
new file mode 100644
index 00000000..7d84d295
--- /dev/null
+++ b/pddl/builders/constants_def.py
@@ -0,0 +1,40 @@
+#
+# Copyright 2021-2023 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pddl.
+#
+# Use of this source code is governed by an MIT-style
+# license that can be found in the LICENSE file or at
+# https://opensource.org/licenses/MIT.
+#
+
+"""This module implements the ConstantsDef class to handle the constants of a PDDL domain."""
+from typing import AbstractSet, Sequence, cast
+
+from pddl.builders.base import _Definition, _Context
+from pddl.builders.terms_list import TermsValidator
+from pddl.logic import Constant
+
+
+class ConstantsDef(_Definition):
+    """A set of constants of a PDDL domain."""
+
+    def __init__(self, context: _Context) -> None:
+        """Initialize the PDDL constants section validator."""
+        super().__init__(context)
+        self._terms_validator = TermsValidator(
+            no_duplicates=True, must_be_instances_of=Constant
+        )
+
+    def add_constant(self, constant: Constant) -> None:
+        """Add a constant."""
+        self._check_typing_requirement_for_term(constant)
+        self._context.check_types_are_available(constant)
+        self._terms_validator.add_term(constant)
+
+    @property
+    def constants(self) -> AbstractSet[Constant]:
+        """Get the constants."""
+        return frozenset(cast(Sequence[Constant], self._terms_validator.terms))
diff --git a/pddl/builders/derived_predicates_def.py b/pddl/builders/derived_predicates_def.py
new file mode 100644
index 00000000..3dd5cec2
--- /dev/null
+++ b/pddl/builders/derived_predicates_def.py
@@ -0,0 +1,67 @@
+#
+# Copyright 2021-2023 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pddl.
+#
+# Use of this source code is governed by an MIT-style
+# license that can be found in the LICENSE file or at
+# https://opensource.org/licenses/MIT.
+#
+
+"""This module implements the DerivedPredicatesDef class to handle derivate predicate definitions of a PDDL domain."""
+from typing import AbstractSet, Set
+
+from pddl.builders.base import _Definition, _Context
+from pddl.logic.predicates import DerivedPredicate
+
+
+class DerivedPredicatesDef(_Definition):
+    """A set of derived predicates of a PDDL domain."""
+
+    def __init__(
+        self,
+        context: _Context,
+    ) -> None:
+        """Initialize the PDDL constants section validator."""
+        super().__init__(context)
+
+        self._derived_predicates: Set[DerivedPredicate] = set()
+        self._check_consistency()
+
+    @property
+    def derived_predicates(self) -> AbstractSet[DerivedPredicate]:
+        """Get the predicates."""
+        return self._derived_predicates
+
+    def _check_consistency(self) -> None:
+        """Check consistency of the derived predicates definition."""
+
+        seen_predicates_by_name: Dict[name_type, Predicate] = {
+            p.name: p for p in self._predicates_def.predicates
+        }
+        for dp in self._derived_predicates:
+            self._check_derived_predicate(dp, seen_predicates_by_name)
+
+    def _check_derived_predicate(
+        self, dp: DerivedPredicate, seen: Dict[name_type, Predicate]
+    ) -> None:
+        if dp.predicate.name in seen:
+            other_p = seen[dp.predicate.name]
+            raise PDDLValidationError(
+                f"the name of derived predicate {dp} has been already used by {other_p}"
+            )
+        seen[dp.predicate.name] = dp.predicate
+        TermsChecker(self._requirements, self._types, check_repetitions=False).check(
+            dp.predicate.terms
+        )
+        variables = {t for t in dp.predicate.terms}
+        FormulaChecker(
+            self._requirements,
+            self._types,
+            self._constants_def.constants,
+            variables,
+            self._predicates_def.predicates,
+            self._derived_predicates,
+        ).check_formula(dp.condition)
\ No newline at end of file
diff --git a/pddl/builders/domain.py b/pddl/builders/domain.py
new file mode 100644
index 00000000..4e4aae23
--- /dev/null
+++ b/pddl/builders/domain.py
@@ -0,0 +1,73 @@
+from typing import Optional, AbstractSet
+
+from pddl.builders.base import BaseBuilder, _Context
+from pddl.builders.constants_def import ConstantsDef
+from pddl.builders.derived_predicates_def import DerivedPredicatesDef
+from pddl.builders.predicates_def import PredicatesDef
+from pddl.custom_types import namelike
+from pddl.logic import Constant, Predicate
+from pddl.requirements import Requirements
+
+
+class DomainBuilder(BaseBuilder):
+    """A builder for PDDL domains."""
+
+    def __init__(self, name: str):
+        """Initialize the domain builder."""
+        self.__name = name
+        self.__context = _Context()
+        self.__constants_def: ConstantsDef = ConstantsDef(self.__context)
+        self.__predicates_def: PredicatesDef = PredicatesDef(self.__context)
+        self.__derived_predicates_def: DerivedPredicatesDef = DerivedPredicatesDef(self.__context)
+
+    @property
+    def requirements(self) -> AbstractSet[Requirements]:
+        """Get the requirements."""
+        return self.__context.requirements
+
+    @property
+    def has_typing(self) -> bool:
+        """Check if the typing requirement is specified."""
+        return self.__context.has_typing
+
+    def add_requirement(self, requirement: Requirements) -> "DomainBuilder":
+        """Add a requirement to the domain."""
+        self.__context.add_requirement(requirement)
+        return self
+
+    def add_type(
+        self, child_type: namelike, parent_type: Optional[namelike] = None
+    ) -> "DomainBuilder":
+        """Add a type to the domain."""
+        self.__context.add_type(child_type, parent_type)
+        return self
+
+    def add_constant(self, constant: Constant) -> "DomainBuilder":
+        """Add a constant to the domain."""
+        self.__constants_def.add_constant(constant)
+        return self
+
+    def add_predicate_def(self, predicate_def: Predicate) -> "DomainBuilder":
+        """
+        Add a predicate definition to the domain.
+
+        The predicate definition must be a predicate with only variables.
+        """
+        self.__predicates_def.add_predicate_def(predicate_def)
+        return self
+
+    def build(self) -> "T":
+        pass
+
+    # def build(self) -> Domain:
+    #     """Build the domain."""
+    #     return Domain(
+    #         name=self.__name,
+    #         requirements=self.__requirements,
+    #         types=self.types,
+    #         constants=self.__constants,
+    #         predicates=self.predicates,
+    #         functions=self.functions,
+    #         actions=self.actions,
+    #         axioms=self.axioms,
+    #     )
diff --git a/pddl/builders/formula_validator.py b/pddl/builders/formula_validator.py
new file mode 100644
index 00000000..9f89be7c
--- /dev/null
+++ b/pddl/builders/formula_validator.py
@@ -0,0 +1,185 @@
+#
+# Copyright 2021-2023 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pddl.
+#
+# Use of this source code is governed by an MIT-style
+# license that can be found in the LICENSE file or at
+# https://opensource.org/licenses/MIT.
+#
+
+"""This module implements a validator class for PDDL formulas."""
+
+import functools
+from typing import AbstractSet, Collection, Mapping
+
+from pddl.builders.base import _Context
+from pddl.builders.constants_def import ConstantsDef
+from pddl.builders.predicates_def import PredicatesDef
+from pddl.builders.types_def import TypesDef
+from pddl.custom_types import name as name_type
+from pddl.exceptions import PDDLValidationError
+from pddl.helpers.base import assert_
+from pddl.logic import Predicate, Variable
+from pddl.logic.base import (
+    BinaryOp,
+    Formula,
+    QuantifiedCondition,
+    UnaryOp,
+)
+from pddl.logic.predicates import DerivedPredicate, EqualTo
+from pddl.logic.terms import Constant, Term, _print_tag_set
+from pddl.requirements import Requirements
+
+
+class FormulaValidator:
+    """Implementation of a type checker for formulas instances."""
+
+    def __init__(
+        self,
+        context: _Context,
+        constants: ConstantsDef,
+        available_predicates: PredicatesDef,
+        available_derived_predicates: Collection[DerivedPredicate],
+        variables: AbstractSet[Variable],
+    ) -> None:
+        """Initialize the formula validator."""
+        self._context = context
+
+        # build a mapping from predicate names to predicates
+        d1 = {p.name: p for p in available_predicates}
+        d2 = {dp.name: dp.predicate for dp in available_derived_predicates}
+        assert_(d1.keys().isdisjoint(d2.keys()))
+        d1.update(d2)
+        self._available_predicates_by_name: Mapping[name_type, Predicate] = d1
+
+        # allowed constants in the formula
+        self._constants_by_name = {c.name: c for c in constants}
+
+        # allowed variables in the formula: this set might change during the type checking
+        # (e.g. when checking quantifiers)
+        self._current_variables_set_by_name = {v.name: v for v in variables}
+
+    def check_formula(self, formula: Formula):
+        """Check types annotations of PDDL data structures."""
+        self._check_formula(formula)
+
+    def _check_variable_is_allowed(self, variable: Variable) -> None:
+        """Check that the variable is allowed in the current scope."""
+        if variable.name not in self._current_variables_set_by_name:
+            raise PDDLValidationError(
+                f"variable {variable} is not allowed in this scope"
+            )
+
+    def _check_constant_is_defined(self, constant: Constant) -> None:
+        """Check that the constant is defined."""
+        self._context.constants_def.check_constant_is_defined(constant)
+
+    def _raise_not_implemented_error(self, obj: object) -> None:
+        """Raise a NotImplementedError for the given object."""
+        raise NotImplementedError(f"cannot check PDDL types of {type(obj)}")
+
+    @functools.singledispatchmethod
+    def _check_formula(self, obj: object) -> None:
+        self._raise_not_implemented_error(obj)
+
+    @_check_formula.register
+    def _(self, term: Term) -> None:
+        """Check types annotations of a PDDL term."""
+        self._check_term(term)
+
+    @_check_formula.register
+    def _(self, constant: Constant) -> None:
+        """Check types annotations of a PDDL constant."""
+        self._check_term(constant)
+        self._check_constant_is_defined(constant)
+
+    @_check_formula.register
+    def _(self, variable: Variable) -> None:
+        """Check types annotations of a PDDL variable."""
+        self._check_term(variable)
+        self._check_variable_is_allowed(variable)
+
+    @_check_formula.register
+    def _(self, predicate: Predicate) -> None:
+        """Check types annotations of a PDDL predicate."""
+        # check that the predicate is available
+        if predicate.name not in self._available_predicates_by_name:
+            raise PDDLValidationError(
+                f"predicate {predicate.name} is not available in the domain"
+            )
+        # check that the predicate has the correct number of arguments
+        available_predicate = self._available_predicates_by_name[predicate.name]
+        if len(predicate.arguments) != len(available_predicate.arguments):
+            raise PDDLValidationError(
+                f"predicate {predicate.name} has {len(available_predicate.arguments)} arguments, "
+                f"but {len(predicate.arguments)} arguments were given"
+            )
+
+        # check that the predicate has the correct types
+        for arg, available_arg in zip(
+            predicate.arguments, available_predicate.arguments
+        ):
+            if not arg.type_tags.issubset(available_arg.type_tags):
+                raise PDDLValidationError(
+                    f"predicate {predicate.name} has argument {arg} with type tags {_print_tag_set(arg.type_tags)}, "
+                    f"but argument {available_arg} has type tags {_print_tag_set(arg.type_tags)}, and there is no"
+                )
+
+        # check that the predicate has valid constants and variables
+        for arg in predicate.arguments:
+            self._check_formula(arg)
+
+    @_check_formula.register
+    def _(self, equal_to: EqualTo) -> None:
+        """Check types annotations of a PDDL equal-to atomic formula."""
+        self._check_formula(equal_to.left)
+        self._check_formula(equal_to.right)
+
+    @_check_formula.register
+    def _(self, derived_predicate: DerivedPredicate) -> None:
+        """Check types annotations of a PDDL derived predicate."""
+        self._raise_not_implemented_error(derived_predicate)
+
+    @_check_formula.register
+    def _(self, formula: UnaryOp) -> None:
+        """Check types annotations of a PDDL unary operator."""
+        self._check_formula(formula.argument)
+
+    @_check_formula.register
+    def _(self, formula: BinaryOp) -> None:
+        """Check types annotations of a PDDL binary operator."""
+        for operand in formula.operands:
+            self._check_formula(operand)
+
+    @_check_formula.register
+    def _(self, formula: TrueFormula) -> None:
+        """Check types annotations of a PDDL true formula."""
+
+    @_check_formula.register
+    def _(self, formula: FalseFormula) -> None:
+        """Check types annotations of a PDDL false formula."""
+
+    @_check_formula.register
+    def _(self, formula: QuantifiedCondition) -> None:
+        """Check types annotations of a PDDL quantified condition."""
+        # quantified condition can add new variables to the scope
+        # check no variable is defined twice
+        for v in formula.variables:
+            if v.name in self._current_variables_set_by_name:
+                raise PDDLValidationError(
+                    f"in scope determined by {formula}, variable {v} is already defined"
+                )
+            self._check_term(v)
+
+        # add new variables to the scope
+        try:
+            self._current_variables_set_by_name.update(
+                {v.name: v for v in formula.variables}
+            )
+            self._check_formula(formula.condition)
+        finally:
+            for v in formula.variables:
+                self._current_variables_set_by_name.pop(v.name)
\ No newline at end of file
diff --git a/pddl/builders/predicates_def.py b/pddl/builders/predicates_def.py
new file mode 100644
index 00000000..629554c5
--- /dev/null
+++ b/pddl/builders/predicates_def.py
@@ -0,0 +1,55 @@
+#
+# Copyright 2021-2023 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pddl.
+#
+# Use of this source code is governed by an MIT-style
+# license that can be found in the LICENSE file or at
+# https://opensource.org/licenses/MIT.
+#
+
+"""This module implements the PredicatesDef class to handle the predicate definitions of a PDDL domain."""
+from typing import Dict, AbstractSet
+
+from pddl.builders.base import _Context, _Definition
+from pddl.builders.terms_list import TermsValidator
+from pddl.custom_types import name as name_type
+from pddl.logic import Variable
+from pddl.logic.predicates import Predicate
+
+
+class PredicatesDef(_Definition):
+    """A set of predicates of a PDDL domain."""
+
+    def __init__(self, context: _Context) -> None:
+        """Initialize the PDDL predicates section validator."""
+        super().__init__(context)
+        self._predicates_by_name: Dict[name_type, Predicate] = {}
+
+    def add_predicate_def(self, predicate_def: Predicate) -> None:
+        """Add a predicate definition."""
+        self._context.check_name_not_already_used(predicate_def.name, predicate_def)
+        self._check_predicates_terms(predicate_def)
+
+        self._predicates_by_name[predicate_def.name] = predicate_def
+        self._context.add_used_name(predicate_def.name, predicate_def)
+
+    @property
+    def predicates(self) -> AbstractSet[Predicate]:
+        """Get the predicates."""
+        return frozenset(self._predicates_by_name.values())
+
+    @property
+    def predicate_names(self) -> AbstractSet[name_type]:
+        """Get the predicates names."""
+        return self._predicates_by_name.keys()
+
+    def _check_predicates_terms(self, predicates_def: Predicate) -> None:
+        """Check that the terms of the predicates are consistent."""
+        validator = TermsValidator(must_be_instances_of=Variable)
+        for term in predicates_def.terms:
+            self._check_typing_requirement_for_term(term)
+            self._context.check_types_are_available(term)
+            validator.add_term(term)
diff --git a/pddl/validation/terms.py b/pddl/builders/terms_list.py
similarity index 56%
rename from pddl/validation/terms.py
rename to pddl/builders/terms_list.py
index 2f03648a..22645d2e 100644
--- a/pddl/validation/terms.py
+++ b/pddl/builders/terms_list.py
@@ -10,82 +10,50 @@
 # https://opensource.org/licenses/MIT.
 #
 
-"""Module for validator of terms."""
-from functools import partial
-from typing import (
-    AbstractSet,
-    Collection,
-    Dict,
-    Generator,
-    Mapping,
-    Optional,
-    Type,
-    Union,
-)
+"""Module for validator of terms lists."""
+from typing import Collection, Dict, List, Optional, Sequence, Type, Union
 
 from pddl.custom_types import name as name_type
-from pddl.definitions.base import TypesDef
 from pddl.exceptions import PDDLValidationError
 from pddl.helpers.base import check
 from pddl.logic.terms import Constant, Term, Variable, _print_tag_set
-from pddl.requirements import Requirements
-from pddl.validation.base import BaseValidator
 
 
-class TermsValidator(BaseValidator):
-    """
-    Class for validator of terms.
-
-    Some machinery is required to make the code as much as reusable as possible.
-    """
+class TermsValidator:
+    """Class for validator of terms."""
 
     def __init__(
         self,
-        requirements: AbstractSet[Requirements],
-        types: TypesDef,
         must_be_instances_of: Optional[Union[Type[Constant], Type[Variable]]] = None,
         no_duplicates: bool = False,
     ):
         """Initialize the validator."""
-        super().__init__(requirements, types)
 
         # if none, then we don't care if constant or variable
         self._allowed_superclass = must_be_instances_of
         self._no_duplicates = no_duplicates
 
-    def check_terms_consistency(self, terms: Collection[Term]):
-        """
-        Check that there are no duplicates.
+        # a dictionary from name to Term, for fast lookup
+        self._seen: Dict[name_type, Term] = {}
 
-        This is the non-iterative version of '_check_terms_consistency_iterator'.
-        """
-        # consume the iterator
-        list(self._check_terms_consistency_iterator(terms))
+        # the full list of terms
+        self._terms: List[Term] = []
 
-    def _check_terms_consistency_iterator(
-        self, terms: Collection[Term]
-    ) -> Generator[Term, None, None]:
-        """
-        Iterate over terms and check that terms with the same name must have the same type tags.
+    @property
+    def terms(self) -> Sequence[Term]:
+        """Get the terms."""
+        return self._terms
 
-        In particular:
-        - if no_duplicates=Term there cannot be terms with the same name (variable or constant);
-        - terms with the same name must be of the same term type (variable or constant);
-        - terms with the same name must have the same type tags.
-        """
-        seen: Dict[name_type, Term] = {}
-        for term in terms:
-            self._check_already_seen_term(term, seen)
-            self._check_same_term_has_same_type_tags(term, seen)
-            self._check_term_type(term, term_type=self._allowed_superclass)
-            yield term
-            seen[term.name] = term
+    @classmethod
+    def check_terms(cls, terms: Collection[Term]):
+        """Check that there are no duplicates."""
+        TermsValidator().add_terms(terms)
 
-    def _check_already_seen_term(self, term: Term, seen: Mapping[name_type, Term]):
+    def _check_already_seen_term(self, term: Term):
         """Check whether a term has been already seen earlier in the terms list."""
-        if self._no_duplicates and term.name in seen:
+        if self._no_duplicates and term.name in self._seen:
             same_name_but_different_type = type(term) is not type(  # noqa: E721
-                seen[term.name]
+                self._seen[term.name]
             )
             check(
                 same_name_but_different_type,
@@ -93,17 +61,14 @@ def _check_already_seen_term(self, term: Term, seen: Mapping[name_type, Term]):
                 exception_cls=PDDLValidationError,
             )
 
-    @classmethod
-    def _check_same_term_has_same_type_tags(
-        cls, term: Term, seen: Dict[name_type, Term]
-    ) -> None:
+    def _check_same_term_has_same_type_tags(self, term: Term) -> None:
         """
         Check if the term has already been seen and, if so, that it has the same type tags.
 
         This is an auxiliary method to simplify the implementation of '_check_terms_consistency_iterator'.
         """
-        if term.name in seen:
-            expected_type_tags = seen[term.name].type_tags
+        if term.name in self._seen:
+            expected_type_tags = self._seen[term.name].type_tags
             actual_type_tags = set(term.type_tags)
             check(
                 expected_type_tags == actual_type_tags,
@@ -127,16 +92,31 @@ def _check_term_type(
                 exception_cls=PDDLValidationError,
             )
 
-    def check_terms(self, terms: Collection[Term]) -> None:
-        """Check the terms."""
-        terms_iter = self._check_terms_consistency_iterator(terms)
-        for term in terms_iter:
-            self._check_typing_requirement(term.type_tags)
-            self._check_types_are_available(
-                term.type_tags, partial(self._terms_to_string, terms)
-            )
+    def add_terms(self, terms: Collection[Term]) -> None:
+        """Perform consistency checks and add a list of terms."""
+        for term in terms:
+            self.add_term(term)
+
+    def check_term(self, term: Term) -> None:
+        """
+        Perform consistency checks against a single term.
+
+        In particular:
+        - if no_duplicates=Term there cannot be terms with the same name (variable or constant);
+        - terms with the same name must be of the same term type (variable or constant);
+        - terms with the same name must have the same type tags.
+        """
+        self._check_already_seen_term(term)
+        self._check_same_term_has_same_type_tags(term)
+        self._check_term_type(term, term_type=self._allowed_superclass)
 
     @classmethod
     def _terms_to_string(cls, terms: Collection[Term]) -> str:
         """Convert terms to string for error messages."""
         return "terms ['" + "', '".join(map(str, terms)) + "']"
+
+    def add_term(self, term: Term) -> None:
+        """Add a single term."""
+        self.check_term(term)
+        self._seen[term.name] = term
+        self._terms.append(term)
diff --git a/pddl/builders/types_def.py b/pddl/builders/types_def.py
new file mode 100644
index 00000000..22ff6984
--- /dev/null
+++ b/pddl/builders/types_def.py
@@ -0,0 +1,156 @@
+#
+# Copyright 2021-2023 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pddl.
+#
+# Use of this source code is governed by an MIT-style
+# license that can be found in the LICENSE file or at
+# https://opensource.org/licenses/MIT.
+#
+
+"""Base module for the PDDL definitions."""
+import bisect
+from typing import AbstractSet, Collection, Dict, List, Mapping, Optional, Sequence, Set
+
+from pddl.custom_types import name as name_type
+from pddl.custom_types import namelike, parse_type, to_names, to_types  # noqa: F401
+from pddl.exceptions import PDDLValidationError
+from pddl.helpers.base import find_cycle, transitive_closure
+from pddl.parser.symbols import Symbols
+
+
+class MutableTypesDef:
+    """A class for representing and managing the types available in a PDDL Domain."""
+
+    def __init__(self) -> None:
+        """Initialize the Types object."""
+        # the types dictionary is a mapping from a type to its parent type (if any)
+        self._types: Dict[name_type, Optional[name_type]] = {}
+
+        # the set of all types
+        self._all_types: Set[name_type] = set()
+
+        # the closure of the types dictionary
+        self._types_closure: Dict[name_type, Set[name_type]] = {}
+
+        # only for printing purposes
+        self._sorted_all_types: List[name_type] = []
+
+    @property
+    def raw(self) -> Mapping[name_type, Optional[name_type]]:
+        """Get the raw types dictionary."""
+        return self._types
+
+    @property
+    def all_types(self) -> AbstractSet[name_type]:
+        """Get all available types."""
+        return self._all_types
+
+    @property
+    def sorted_all_types(self) -> Sequence[name_type]:
+        """Get all available types (sorted for printing purposes)."""
+        return self._sorted_all_types
+
+    def are_types_available(self, type_tags: Collection[namelike]) -> bool:
+        """Check whether all the types in type_tags are available."""
+        return self._all_types.issuperset(type_tags)
+
+    def is_subtype(self, type_a: name_type, type_b: name_type) -> bool:
+        """Check if type_a is a subtype of type_b."""
+        # check whether type_a and type_b are legal types
+        error_msg = "type {0} is not in available types {1}"
+        if type_a not in self._all_types:
+            raise PDDLValidationError(
+                error_msg.format(repr(type_a), self._sorted_all_types)
+            )
+        if type_b not in self._all_types:
+            raise PDDLValidationError(
+                error_msg.format(repr(type_b), self._sorted_all_types)
+            )
+
+        return type_a in self._types_closure.get(type_b, set())
+
+    def _compute_types_closure(self) -> Mapping[name_type, Set[name_type]]:
+        """Compute the closure of the types dictionary."""
+        return transitive_closure(self._types)
+
+    def add_type(self, child_type: namelike, parent_type: Optional[namelike] = None):
+        """
+        Add a new type to the types definitions.
+
+        Before adding the new information, this method performs the following checks:
+        - both the child type and the parent type are valid types
+        - the child type is not already defined
+        - the child type is not `object`
+        - the introduction of the new type relation does not create a cycle
+        """
+        # the child type is a valid type
+        child_type = parse_type(child_type)
+        # the parent type (if any) is a valid type
+        parent_type = parse_type(parent_type) if parent_type else None
+
+        # the child type is not already defined
+        self._check_type_already_defined(child_type)
+
+        # the child type is not `object`
+        self._check_child_type_is_not_object(child_type, parent_type)
+
+        # the introduction of the new type relation does not create a cycle
+        self._check_cycle_not_created(child_type, parent_type)
+
+        # add the new type relation
+        self._add_type(child_type, parent_type)
+
+    def _check_type_already_defined(self, child_type: name_type) -> None:
+        """Check that the child type is not already defined."""
+        if child_type in self._types:
+            raise PDDLValidationError(
+                "type '" + str(child_type) + "' is already defined"
+            )
+
+    @classmethod
+    def _check_child_type_is_not_object(
+        cls, child_type: name_type, parent_type: Optional[name_type]
+    ) -> None:
+        """Check that the child type is not `object`."""
+        if child_type == Symbols.OBJECT and parent_type is not None:
+            raise PDDLValidationError(
+                "the type `object` must not have supertypes, but got it is a subtype of '"
+                + str(parent_type)
+                + "'"
+            )
+
+    def _check_cycle_not_created(
+        self, child_type: name_type, parent_type: Optional[name_type]
+    ) -> None:
+        """Check that the introduction of the new type relation does not create a cycle."""
+        # the introduction of the new type relation does not create a cycle
+        if parent_type is not None:
+            # TODO make it more efficient (i.e. detect cycles incrementally)
+            new_types_dict = self._types.copy()
+            new_types_dict[child_type] = parent_type
+            cycle = find_cycle(new_types_dict)
+            if cycle:
+                raise PDDLValidationError(
+                    "the introduction of the new type relation '"
+                    + str(child_type)
+                    + " is a subtype of '"
+                    + str(parent_type)
+                    + "' creates a cycle: "
+                    + " -> ".join(map(str, cycle))
+                )
+
+    def _add_type(self, child_type: name_type, parent_type: Optional[name_type] = None):
+        """Add the new type relation."""
+        self._types[child_type] = parent_type
+        self._all_types.add(child_type)
+        self._all_types.add(parent_type) if parent_type else None
+        # TODO: avoid recomputing the closure, make it incremental
+        self._types_closure = self._compute_types_closure()
+        bisect.insort(self._sorted_all_types, child_type)
+
+
+class TypesDef(MutableTypesDef):
+    pass
diff --git a/pddl/core.py b/pddl/core.py
index 19826a59..3ad20a13 100644
--- a/pddl/core.py
+++ b/pddl/core.py
@@ -21,9 +21,9 @@
 from pddl.action import Action
 from pddl.custom_types import name as name_type
 from pddl.custom_types import namelike, parse_name, to_names, to_types  # noqa: F401
-from pddl.definitions.base import TypesDef
 from pddl.definitions.constants_def import ConstantsDef
 from pddl.definitions.predicates_def import PredicatesDef
+from pddl.definitions.types_def import TypesDef
 from pddl.helpers.base import assert_, check, ensure, ensure_set
 from pddl.logic.base import And, Formula, is_literal
 from pddl.logic.predicates import DerivedPredicate, Predicate
diff --git a/pddl/definitions/__init__.py b/pddl/definitions/__init__.py
deleted file mode 100644
index e567251a..00000000
--- a/pddl/definitions/__init__.py
+++ /dev/null
@@ -1,13 +0,0 @@
-#
-# Copyright 2021-2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of pddl.
-#
-# Use of this source code is governed by an MIT-style
-# license that can be found in the LICENSE file or at
-# https://opensource.org/licenses/MIT.
-#
-
-"""This package includes PDDL definitions classes useful for validation of PDDL domains/problems."""
diff --git a/pddl/definitions/base.py b/pddl/definitions/base.py
deleted file mode 100644
index 746cb1b1..00000000
--- a/pddl/definitions/base.py
+++ /dev/null
@@ -1,166 +0,0 @@
-#
-# Copyright 2021-2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of pddl.
-#
-# Use of this source code is governed by an MIT-style
-# license that can be found in the LICENSE file or at
-# https://opensource.org/licenses/MIT.
-#
-
-"""Base module for the PDDL definitions."""
-from typing import AbstractSet, Dict, FrozenSet, Mapping, Optional, Set, cast
-
-from pddl.custom_types import name as name_type
-from pddl.custom_types import namelike, to_names, to_types  # noqa: F401
-from pddl.exceptions import PDDLValidationError
-from pddl.helpers.base import (
-    assert_,
-    ensure,
-    ensure_set,
-    find_cycle,
-    transitive_closure,
-)
-from pddl.parser.symbols import Symbols
-from pddl.requirements import Requirements
-
-
-class TypesDef:
-    """A class for representing and managing the types available in a PDDL Domain."""
-
-    def __init__(
-        self,
-        types: Optional[Dict[namelike, Optional[namelike]]] = None,
-        requirements: Optional[AbstractSet[Requirements]] = None,
-        skip_checks: bool = False,
-    ) -> None:
-        """Initialize the Types object."""
-        self._types = to_types(ensure(types, dict()))
-
-        if not skip_checks:
-            self._check_types_dictionary(self._types, ensure_set(requirements))
-
-        self._all_types = self._get_all_types()
-        self._types_closure = self._compute_types_closure()
-
-        # only for printing purposes
-        self._sorted_all_types = sorted(self._all_types)
-
-    @property
-    def raw(self) -> Mapping[name_type, Optional[name_type]]:
-        """Get the raw types dictionary."""
-        return self._types
-
-    @property
-    def all_types(self) -> FrozenSet[name_type]:
-        """Get all available types."""
-        return self._all_types
-
-    def is_subtype(self, type_a: name_type, type_b: name_type) -> bool:
-        """Check if type_a is a subtype of type_b."""
-        # check whether type_a and type_b are legal types
-        error_msg = "type {0} is not in available types {1}"
-        if type_a not in self._all_types:
-            raise PDDLValidationError(
-                error_msg.format(repr(type_a), self._sorted_all_types)
-            )
-        if type_b not in self._all_types:
-            raise PDDLValidationError(
-                error_msg.format(repr(type_b), self._sorted_all_types)
-            )
-
-        return type_a in self._types_closure.get(type_b, set())
-
-    def _get_all_types(self) -> FrozenSet[name_type]:
-        """Get all types supported by the domain."""
-        if self._types is None:
-            return frozenset()
-        result = set(self._types.keys()) | set(self._types.values())
-        result.discard(None)
-        return cast(FrozenSet[name_type], frozenset(result))
-
-    def _compute_types_closure(self) -> Mapping[name_type, Set[name_type]]:
-        """Compute the closure of the types dictionary."""
-        return transitive_closure(self._types)
-
-    @classmethod
-    def _check_types_dictionary(
-        cls,
-        type_dict: Mapping[name_type, Optional[name_type]],
-        requirements: AbstractSet[Requirements],
-    ) -> None:
-        """
-        Check the consistency of the types dictionary.
-
-        1) Empty types dictionary is correct by definition:
-        >>> TypesDef._check_types_dictionary({}, set())
-
-        2) There are supertypes, but :typing requirement not specified
-        >>> a, b, c = to_names(["a", "b", "c"])
-        >>> TypesDef._check_types_dictionary({a: b, b: c}, set())
-        Traceback (most recent call last):
-        ...
-        pddl.exceptions.PDDLValidationError: typing requirement is not specified, but types are used: 'b', 'c'
-
-        3) The `object` type cannot be a subtype:
-        >>> a = name_type("a")
-        >>> TypesDef._check_types_dictionary({name_type("object"): a}, {Requirements.TYPING})
-        Traceback (most recent call last):
-        ...
-        pddl.exceptions.PDDLValidationError: object must not have supertypes, but got 'object' is a subtype of 'a'
-
-        4) If cycles in the type hierarchy graph are present, an error is raised:
-        >>> a, b, c = to_names(["a", "b", "c"])
-        >>> TypesDef._check_types_dictionary({a: b, b: c, c: a}, {Requirements.TYPING})
-        Traceback (most recent call last):
-        ...
-        pddl.exceptions.PDDLValidationError: cycle detected in the type hierarchy: a -> b -> c
-
-        :param type_dict: the types dictionary
-        """
-        if len(type_dict) == 0:
-            return
-
-        # check typing requirement
-        supertypes = {t for t in type_dict.values() if t is not None}
-        if len(supertypes) > 0 and Requirements.TYPING not in requirements:
-            raise PDDLValidationError(
-                "typing requirement is not specified, but types are used: '"
-                + "', '".join(map(str, sorted(supertypes)))
-                + "'"
-            )
-
-        # check `object` type
-        object_name = name_type(Symbols.OBJECT.value)
-        if object_name in type_dict and type_dict[object_name] is not None:
-            object_supertype = type_dict[object_name]
-            raise PDDLValidationError(
-                f"object must not have supertypes, but got 'object' is a subtype of '{object_supertype}'"
-            )
-
-        # check cycles
-        # need to convert type_dict to a dict of sets, because find_cycle() expects a dict of sets
-        cycle = find_cycle(
-            {
-                key: {value} if value is not None else set()
-                for key, value in type_dict.items()
-            }
-        )  # type: ignore
-        if cycle is not None:
-            raise PDDLValidationError(
-                "cycle detected in the type hierarchy: " + " -> ".join(cycle)
-            )
-
-
-class _Definition:
-    """Abstract class for a PDDL definition."""
-
-    def __init__(
-        self, requirements: AbstractSet[Requirements], types: TypesDef
-    ) -> None:
-        """Initialize the PDDL definition."""
-        assert_(type(self) is not _Definition)
-        self._requirements = requirements
-        self._types = types
diff --git a/pddl/definitions/constants_def.py b/pddl/definitions/constants_def.py
deleted file mode 100644
index 9f6032f5..00000000
--- a/pddl/definitions/constants_def.py
+++ /dev/null
@@ -1,43 +0,0 @@
-#
-# Copyright 2021-2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of pddl.
-#
-# Use of this source code is governed by an MIT-style
-# license that can be found in the LICENSE file or at
-# https://opensource.org/licenses/MIT.
-#
-
-"""This module implements the ConstantsDef class to handle the constants of a PDDL domain."""
-from typing import AbstractSet, Collection, Optional
-
-from pddl.definitions.base import TypesDef, _Definition
-from pddl.helpers.base import ensure_set
-from pddl.logic import Constant
-from pddl.requirements import Requirements
-from pddl.validation.terms import TermsValidator
-
-
-class ConstantsDef(_Definition):
-    """A set of constants of a PDDL domain."""
-
-    def __init__(
-        self,
-        requirements: AbstractSet[Requirements],
-        types: TypesDef,
-        constants: Optional[Collection[Constant]],
-    ) -> None:
-        """Initialize the PDDL constants section validator."""
-        TermsValidator(requirements, types, no_duplicates=True).check_terms(
-            constants if constants else []
-        )
-
-        super().__init__(requirements, types)
-        self._constants = ensure_set(constants)
-
-    @property
-    def constants(self) -> AbstractSet[Constant]:
-        """Get the constants."""
-        return self._constants
diff --git a/pddl/definitions/predicates_def.py b/pddl/definitions/predicates_def.py
deleted file mode 100644
index 0f0aaf91..00000000
--- a/pddl/definitions/predicates_def.py
+++ /dev/null
@@ -1,61 +0,0 @@
-#
-# Copyright 2021-2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of pddl.
-#
-# Use of this source code is governed by an MIT-style
-# license that can be found in the LICENSE file or at
-# https://opensource.org/licenses/MIT.
-#
-
-"""This module implements the ConstantsDef class to handle the constants of a PDDL domain."""
-from typing import AbstractSet, Collection, Dict, Optional
-
-from pddl.custom_types import name as name_type
-from pddl.definitions.base import TypesDef, _Definition
-from pddl.exceptions import PDDLValidationError
-from pddl.helpers.base import ensure_set
-from pddl.logic import Variable
-from pddl.logic.predicates import Predicate
-from pddl.requirements import Requirements
-from pddl.validation.terms import TermsValidator
-
-
-class PredicatesDef(_Definition):
-    """A set of predicates of a PDDL domain."""
-
-    def __init__(
-        self,
-        requirements: AbstractSet[Requirements],
-        types: TypesDef,
-        predicates: Optional[Collection[Predicate]],
-    ) -> None:
-        """Initialize the PDDL constants section validator."""
-        super().__init__(requirements, types)
-
-        self._predicates: AbstractSet[Predicate] = ensure_set(predicates)
-
-        self._check_consistency()
-
-    @property
-    def predicates(self) -> AbstractSet[Predicate]:
-        """Get the predicates."""
-        return self._predicates
-
-    def _check_consistency(self) -> None:
-        """Check consistency of the predicates definition."""
-        seen_predicates_by_name: Dict[name_type, Predicate] = {}
-        for p in self._predicates:
-            # check that no two predicates have the same name
-            if p.name in seen_predicates_by_name:
-                raise PDDLValidationError(
-                    f"these predicates have the same name: {p}, {seen_predicates_by_name[p.name]}"
-                )
-            seen_predicates_by_name[p.name] = p
-
-            # check that the terms are consistent wrt types, and that are all variables
-            TermsValidator(
-                self._requirements, self._types, must_be_instances_of=Variable
-            ).check_terms(p.terms)
diff --git a/pddl/logic/predicates.py b/pddl/logic/predicates.py
index dce94ab3..69e31014 100644
--- a/pddl/logic/predicates.py
+++ b/pddl/logic/predicates.py
@@ -16,13 +16,11 @@
 
 from pddl.custom_types import name as name_type
 from pddl.custom_types import namelike, parse_name
-from pddl.definitions.base import TypesDef
 from pddl.helpers.base import assert_
 from pddl.helpers.cache_hash import cache_hash
 from pddl.logic.base import Atomic, Formula
 from pddl.logic.terms import Constant, Term
 from pddl.parser.symbols import Symbols
-from pddl.requirements import Requirements
 from pddl.validation.terms import TermsValidator
 
 
@@ -51,7 +49,7 @@ def _check_terms_light(self, terms: Sequence[Term]) -> None:
 
         This method only performs checks that do not require external information (e.g. types provided by the domain).
         """
-        TermsValidator({Requirements.TYPING}, TypesDef()).check_terms_consistency(terms)
+        TermsValidator.check_terms(terms)
 
 
 @cache_hash
diff --git a/pddl/validation/base.py b/pddl/validation/base.py
deleted file mode 100644
index a24ab3da..00000000
--- a/pddl/validation/base.py
+++ /dev/null
@@ -1,53 +0,0 @@
-#
-# Copyright 2021-2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of pddl.
-#
-# Use of this source code is governed by an MIT-style
-# license that can be found in the LICENSE file or at
-# https://opensource.org/licenses/MIT.
-#
-
-"""Base module for validators."""
-from typing import AbstractSet, Callable, Collection
-
-from pddl.custom_types import name as name_type
-from pddl.definitions.base import TypesDef
-from pddl.exceptions import PDDLValidationError
-from pddl.helpers.base import assert_
-from pddl.requirements import Requirements
-
-
-class BaseValidator:
-    """Base class for validators."""
-
-    def __init__(
-        self, requirements: AbstractSet[Requirements], types: TypesDef
-    ) -> None:
-        """Initialize the validator."""
-        assert_(type(self) is not BaseValidator)
-        self._requirements = requirements
-        self._types = types
-
-    @property
-    def has_typing(self) -> bool:
-        """Check if the typing requirement is specified."""
-        return Requirements.TYPING in self._requirements
-
-    def _check_typing_requirement(self, type_tags: Collection[name_type]) -> None:
-        """Check that the typing requirement is specified."""
-        if not self.has_typing and len(type_tags) > 0:
-            raise PDDLValidationError(
-                f"typing requirement is not specified, but the following types were used: {type_tags}"
-            )
-
-    def _check_types_are_available(
-        self, type_tags: Collection[name_type], what: Callable[[], str]
-    ) -> None:
-        """Check that the types are available in the domain."""
-        if not self._types.all_types.issuperset(type_tags):
-            raise PDDLValidationError(
-                f"types {sorted(type_tags)} of {what()} are not in available types {sorted(self._types.all_types)}"
-            )