diff --git a/docs/make.jl b/docs/make.jl
index ba9a64a1..8d3db894 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -13,6 +13,7 @@ makedocs(
         "User interface" => "lib/interface.md",
         "Systems" => "lib/systems.md",
         "Algorithms" => "lib/algorithms.md",
+        "Properties" => "lib/properties.md",
         "Transformations" => "lib/transformations.md",
         "Discretization" => "lib/discretize.md",
         "Distributed computations" => "lib/distributed.md"],
diff --git a/docs/src/lib/properties.md b/docs/src/lib/properties.md
new file mode 100644
index 00000000..d20432f5
--- /dev/null
+++ b/docs/src/lib/properties.md
@@ -0,0 +1,37 @@
+# Properties
+
+This module provides representations of (safety) properties.
+
+```@contents
+Pages = ["properties.md"]
+Depth = 3
+```
+
+```@meta
+CurrentModule = Reachability.Properties
+```
+
+## General property interface
+
+```@docs
+Property
+```
+
+### Boolean combination of properties
+
+```@docs
+Conjunction
+check(::Conjunction, ::LazySet)
+Disjunction
+check(::Disjunction, ::LazySet)
+```
+
+### Specific properties
+
+
+```@docs
+SafeStatesProperty
+check(::SafeStatesProperty, ::LazySet)
+BadStatesProperty
+check(::BadStatesProperty, ::LazySet)
+```
diff --git a/src/Properties/BadStatesProperty.jl b/src/Properties/BadStatesProperty.jl
new file mode 100644
index 00000000..d4e38f8f
--- /dev/null
+++ b/src/Properties/BadStatesProperty.jl
@@ -0,0 +1,55 @@
+"""
+    BadStatesProperty{N<:Real} <: Property
+
+Type that represents a safety property characterized by a set of bad states.
+The property is satisfied by a given set of states if the intersection with the
+set of bad states is empty.
+
+### Fields
+
+- `bad`     -- convex set representing the bad states
+- `witness` -- witness point (empty vector if not set)
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a safety
+property characterized by a set of bad states 𝑃:
+
+```math
+    X \\models 𝑃 \\iff X ∩ 𝑃.\\texttt{bad} = ∅
+```
+"""
+mutable struct BadStatesProperty{N<:Real} <: Property
+    bad::LazySet
+    witness::Vector{N}
+
+    BadStatesProperty{N}(bad::LazySet) where {N<:Real} = new(bad, N[])
+end
+
+# type-less convenience constructor
+BadStatesProperty(bad::LazySet{N}) where {N<:Real} =
+    BadStatesProperty{N}(bad)
+
+"""
+    check(𝑃::BadStatesProperty, X::LazySet)::Bool
+
+Checks whether a convex set is disjoint from the set of bad states.
+
+### Input
+
+- `𝑃` -- safety property with bad states
+- `X` -- convex set
+
+### Output
+
+`true` iff the given set of states does not intersect with the set of bad
+states.
+"""
+@inline function check(𝑃::BadStatesProperty, X::LazySet)::Bool
+    empty_intersection, witness = is_intersection_empty(X, 𝑃.bad, true)
+    if !empty_intersection
+        # store violation witness
+        𝑃.witness = witness
+    end
+    return empty_intersection
+end
diff --git a/src/Properties/Conjunction.jl b/src/Properties/Conjunction.jl
new file mode 100644
index 00000000..df589c0e
--- /dev/null
+++ b/src/Properties/Conjunction.jl
@@ -0,0 +1,44 @@
+"""
+    Conjunction <: Property
+
+Type that represents a conjunction of properties.
+
+### Fields
+
+- `conjuncts` -- vector of properties
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a disjunction
+``𝑃 = 𝑃_1 ∧ 𝑃_2 ∧ … ∧ 𝑃_m``:
+
+```math
+    X \\models 𝑃 \\iff X \\models 𝑃_j \\text{ for all } 1 ≤ j ≤ m
+```
+"""
+struct Conjunction <: Property
+    conjuncts::Vector{Property}
+end
+
+"""
+    check(𝑃::Conjunction, X::LazySet)::Bool
+
+Check whether a convex set satisfies a conjunction of properties.
+
+### Input
+
+- `𝑃` -- conjunction of properties
+- `X` -- convex set
+
+### Output
+
+`true` iff `X` satisfies the conjunction of properties `𝑃`.
+"""
+function check(𝑃::Conjunction, X::LazySet)::Bool
+    for conjunct in 𝑃.conjuncts
+        if !check(conjunct, X)
+            return false
+        end
+    end
+    return true
+end
diff --git a/src/Properties/Disjunction.jl b/src/Properties/Disjunction.jl
new file mode 100644
index 00000000..897d3384
--- /dev/null
+++ b/src/Properties/Disjunction.jl
@@ -0,0 +1,74 @@
+"""
+    Disjunction <: Property
+
+Type that represents a disjunction of properties.
+
+### Fields
+
+- `disjuncts` -- vector of properties (elements are reordered by this type)
+- `reorder`   -- flag to indicate whether shuffling is allowed
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a disjunction
+``𝑃 = 𝑃_1 ∨ 𝑃_2 ∨ … ∨ 𝑃_m``:
+
+```math
+    X \\models 𝑃 \\iff X \\models 𝑃_j \\text{ for some } 1 ≤ j ≤ m
+```
+
+If the `reorder` flag is set, the disjuncts may be reordered after each call to
+[`check(𝑃::Disjunction, X::LazySet)`](@ref) as a heuristics to make subsequent
+checks faster.
+"""
+struct Disjunction <: Property
+    disjuncts::Vector{Property}
+    reorder::Bool
+end
+
+# default constructor with activated reordering
+Disjunction(disjuncts::Vector{<:Property}) = Disjunction(disjuncts, true)
+
+"""
+    check(𝑃::Disjunction, X::LazySet)::Bool
+
+Check whether a convex set satisfies a disjunction of properties.
+
+### Input
+
+- `𝑃` -- disjunction of properties
+- `X` -- convex set
+
+### Output
+
+`true` iff `X` satisfies the disjunction of properties `𝑃`.
+
+### Notes
+
+If the `𝑃.reorder` flag is set, the disjuncts may be reordered as a heuristics
+to make subsequent checks faster.
+Since we check satisfaction from left to right, we move the disjunct for which
+satisfaction was established to the front.
+"""
+function check(𝑃::Disjunction, X::LazySet)::Bool
+    for (i, conjunct) in enumerate(𝑃.disjuncts)
+        if check(conjunct, X)
+            _reorder!(𝑃, i)
+            return true
+        end
+    end
+    return false
+end
+
+function _reorder!(𝑃::Disjunction, i::Int)
+    if !𝑃.reorder || i == 1
+        return nothing
+    end
+    first = 𝑃.disjuncts[i]
+    while i > 1
+        𝑃.disjuncts[i] = 𝑃.disjuncts[i-1]
+        i -= 1
+    end
+    𝑃.disjuncts[1] = first
+    return nothing
+end
diff --git a/src/Properties/Properties.jl b/src/Properties/Properties.jl
new file mode 100644
index 00000000..e4e0db62
--- /dev/null
+++ b/src/Properties/Properties.jl
@@ -0,0 +1,27 @@
+__precompile__()
+"""
+Module for defining and checking properties.
+"""
+module Properties
+
+using LazySets
+
+# ==============================
+# Property struct and evaluation
+# ==============================
+include("Property.jl")
+export Property,
+       check
+
+include("Conjunction.jl")
+include("Disjunction.jl")
+export Conjunction,
+       Disjunction
+
+include("BadStatesProperty.jl")
+export BadStatesProperty
+
+include("SafeStatesProperty.jl")
+export SafeStatesProperty
+
+end # module
diff --git a/src/Properties/Property.jl b/src/Properties/Property.jl
new file mode 100644
index 00000000..29adbe4b
--- /dev/null
+++ b/src/Properties/Property.jl
@@ -0,0 +1,7 @@
+"""
+Abstract supertype of properties that can be checked.
+
+Every concrete subtype should provide the following function:
+  - `check(𝑃::Property, X::LazySet)::Bool`
+"""
+abstract type Property end
diff --git a/src/Properties/SafeStatesProperty.jl b/src/Properties/SafeStatesProperty.jl
new file mode 100644
index 00000000..232034e0
--- /dev/null
+++ b/src/Properties/SafeStatesProperty.jl
@@ -0,0 +1,53 @@
+"""
+    SafeStatesProperty{N<:Real} <: Property
+
+Type that represents a safety property characterized by a set of safe states.
+The property is satisfied by a given set of states ``X`` if ``X`` is fully
+contained in the set of safe states.
+
+### Fields
+
+- `safe`    -- convex set representing the safe states
+- `witness` -- witness point (empty vector if not set)
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a safety
+property characterized by a set of safe states 𝑃:
+
+```math
+    X \\models 𝑃 \\iff X ⊆ 𝑃.\\texttt{safe}
+```
+"""
+mutable struct SafeStatesProperty{N<:Real} <: Property
+    safe::LazySet
+    witness::Vector{N}
+
+    SafeStatesProperty{N}(safe::LazySet) where {N<:Real} = new(safe, N[])
+end
+
+# type-less convenience constructor
+SafeStatesProperty(safe::LazySet{N}) where {N<:Real} = SafeStatesProperty{N}(safe)
+
+"""
+    check(𝑃::SafeStatesProperty, X::LazySet)::Bool
+
+Checks whether a convex set is contained in the set of safe states.
+
+### Input
+
+- `𝑃` -- safety property with safe states
+- `X` -- convex set
+
+### Output
+
+`true` iff the given set of states is a subset of the set of safe states.
+"""
+@inline function check(𝑃::SafeStatesProperty, X::LazySet)::Bool
+    is_subset, witness = ⊆(X, 𝑃.safe, true)
+    if !is_subset
+        # store violation witness
+        𝑃.witness = witness
+    end
+    return is_subset
+end
diff --git a/src/ReachSets/Properties/CheckSolution.jl b/src/ReachSets/CheckSolution.jl
similarity index 100%
rename from src/ReachSets/Properties/CheckSolution.jl
rename to src/ReachSets/CheckSolution.jl
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl
index 4552aacc..33c42d84 100644
--- a/src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl
+++ b/src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl
@@ -36,7 +36,7 @@ function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -74,7 +74,7 @@ function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
             Xhatk[i] = (U == nothing ? Xhatk_bi : Xhatk_bi + Whatk[i])
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
@@ -113,7 +113,7 @@ function check_blocks(ϕ::AbstractMatrix{NUM},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -153,7 +153,7 @@ function check_blocks(ϕ::AbstractMatrix{NUM},
             Xhatk[i] = MinkowskiSumArray(arr)
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
@@ -194,7 +194,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -237,7 +237,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
             end
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
@@ -269,7 +269,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -313,7 +313,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
             end
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
index 70197837..b0356d2b 100644
--- a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
+++ b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
@@ -1,4 +1,4 @@
-import LazySets.CacheMinkowskiSum
+using LazySets: CacheMinkowskiSum
 
 """
     check_property(S, property, options)
@@ -77,7 +77,7 @@ function check_property(S::IVP{<:AbstractDiscreteSystem},
         else
             Xhat0_mod = CartesianProductArray(Xhat0)
         end
-        return check_property(Xhat0_mod, property) ? 0 : 1
+        return check(property, Xhat0_mod) ? 0 : 1
     end
     push!(args, Xhat0)
 
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/partitions.jl b/src/ReachSets/ContinuousPost/BFFPSV18/partitions.jl
index 518df831..3f0b7ad9 100644
--- a/src/ReachSets/ContinuousPost/BFFPSV18/partitions.jl
+++ b/src/ReachSets/ContinuousPost/BFFPSV18/partitions.jl
@@ -1,15 +1,15 @@
 """
-    inout_map_property(prop::IntersectionProperty,
+    inout_map_property(𝑃::PROPERTY,
                        partition::AbstractVector{<:AbstractVector{Int}},
                        blocks::AbstractVector{Int},
                        n::Int
-                      )::IntersectionProperty
+                      )::PROPERTY where {PROPERTY<:Property}
 
-Map an `IntersectionProperty` to the dimensions of analyzed blocks.
+Map a property to the dimensions of analyzed blocks.
 
 ### Input
 
-- `prop`      -- property
+- `𝑃`         -- property
 - `partition` -- block partition; elements are start and end indices of a block
 - `blocks`    -- list of all output block indices in the partition
 - `n`         -- total number of input dimensions
@@ -20,80 +20,50 @@ A new property of reduced dimension.
 
 ### Notes
 
-If the dimension is not reduced, we keep the original set.
-Otherwise, the dimension reduction is achieved with a `LinearMap`.
+If the dimension is not reduced, we return the original property.
+Otherwise, the dimension reduction is implemented via a (lazy) `LinearMap`.
 """
-function inout_map_property(prop::IntersectionProperty{N},
+function inout_map_property(𝑃::PROPERTY,
                             partition::AbstractVector{<:AbstractVector{Int}},
                             blocks::AbstractVector{Int},
                             n::Int
-                           )::IntersectionProperty{N} where {N<:Real}
-    @assert dim(prop.bad) == n "the property has dimension $(dim(prop.bad)) but should have dimension $n"
+                           )::PROPERTY where {PROPERTY<:Property}
     proj = projection_map(partition, blocks)
     if length(proj) == n
-        # no change in the dimension, copy the old property (keep the set)
-        return IntersectionProperty(prop.bad)
+        # no change in the dimension, return the original property
+        return 𝑃
     else
-        M = sparse(proj, proj, ones(N, length(proj)), n, n)
-        return IntersectionProperty(M * prop.bad)
+        M = sparse(proj, proj, ones(length(proj)), n, n)
+        return inout_map_property_helper(𝑃, M)
     end
 end
 
-"""
-    inout_map_property(prop::LinearConstraintProperty{N},
-                       partition::AbstractVector{<:AbstractVector{Int}},
-                       blocks::AbstractVector{Int},
-                       n::Int
-                      )::LinearConstraintProperty{N} where {N<:Real}
-
-Map a `LinearConstraintProperty` to the dimensions of analyzed blocks.
-
-### Input
-
-- `prop`      -- property
-- `partition` -- block partition; elements are start and end indices of a block
-- `blocks`    -- list of all output block indices in the partition
-- `n`         -- total number of input dimensions
-
-### Output
-
-A new property of reduced dimension.
-"""
-function inout_map_property(prop::LinearConstraintProperty{N},
-                            partition::AbstractVector{<:AbstractVector{Int}},
-                            blocks::AbstractVector{Int},
-                            n::Int
-                           )::LinearConstraintProperty{N} where {N<:Real}
-    # sanity check: do not project away non-zero dimensions
-    function check_projection(a, proj)
-        p = 1
-        for i in 1:length(a)
-            if p <= length(proj) && i == proj[p]
-                # dimension is not projected away
-                p += 1
-            elseif a[i] != 0
-                # dimension is projected away; entry is non-zero
-                return false
-            end
-        end
-        return true
+function inout_map_property_helper(𝑃::Conjunction, M::AbstractMatrix)
+    new_conjuncts = similar(𝑃.conjuncts)
+    for (i, conjunct) in enumerate(𝑃.conjuncts)
+        new_conjuncts[i] = inout_map_property_helper(conjunct, M)
     end
+    return Conjunction(new_conjuncts)
+end
 
-    @assert dim(prop.clauses[1].atoms[1]) == n "the property has dimension $(dim(prop.clauses[1].atoms[1])) but should have dimension $n"
+function inout_map_property_helper(𝑃::Disjunction, M::AbstractMatrix)
+    new_disjuncts = similar(𝑃.disjuncts)
+    for (i, disjunct) in enumerate(𝑃.disjuncts)
+        new_disjuncts[i] = inout_map_property_helper(disjunct, M)
+    end
+    return Disjunction(new_disjuncts)
+end
 
-    proj = projection_map(partition, blocks)
+function inout_map_property_helper(𝑃::BadStatesProperty, M::AbstractMatrix)
+    @assert dim(𝑃.bad) == size(M, 2) "the property has dimension " *
+        "$(dim(𝑃.bad)) but should have dimension $(size(M, 2))"
+    return BadStatesProperty(M * 𝑃.bad)
+end
 
-    # create modified property
-    clauses = Vector{Clause{N}}(undef, length(prop.clauses))
-    for (ic, c) in enumerate(prop.clauses)
-        atoms = Vector{LinearConstraint{N}}(undef, length(c.atoms))
-        for (ia, atom) in enumerate(c.atoms)
-            @assert check_projection(atom.a, proj) "blocks incompatible with property"
-            atoms[ia] = LinearConstraint{N}(atom.a[proj], atom.b)
-        end
-        clauses[ic] = Clause(atoms)
-    end
-    return LinearConstraintProperty(clauses)
+function inout_map_property_helper(𝑃::SafeStatesProperty, M::AbstractMatrix)
+    @assert dim(𝑃.safe) == size(M, 2) "the property has dimension " *
+        "$(dim(𝑃.safe)) but should have dimension $(size(M, 2))"
+    return SafeStatesProperty(M * 𝑃.safe)
 end
 
 """
@@ -123,44 +93,3 @@ function projection_map(partition::AbstractVector{<:AbstractVector{Int}},
     end
     return proj
 end
-
-"""
-    inout_map_property(prop::SubsetProperty,
-                       partition::AbstractVector{<:AbstractVector{Int}},
-                       blocks::AbstractVector{Int},
-                       n::Int
-                      )::SubsetProperty
-
-Map an `SubsetProperty` to the dimensions of analyzed blocks.
-
-### Input
-
-- `prop`      -- property
-- `partition` -- block partition; elements are start and end indices of a block
-- `blocks`    -- list of all output block indices in the partition
-- `n`         -- total number of input dimensions
-
-### Output
-
-A new property of reduced dimension.
-
-### Notes
-
-If the dimension is not reduced, we keep the original set.
-Otherwise, the dimension reduction is achieved with a `LinearMap`.
-"""
-function inout_map_property(prop::SubsetProperty{N},
-                            partition::AbstractVector{<:AbstractVector{Int}},
-                            blocks::AbstractVector{Int},
-                            n::Int
-                           )::SubsetProperty{N} where {N<:Real}
-    @assert dim(prop.safe) == n "the property has dimension $(dim(prop.safe)) but should have dimension $n"
-    proj = projection_map(partition, blocks)
-    if length(proj) == n
-        # no change in the dimension, copy the old property (keep the set)
-        return IntersectionProperty(prop.safe)
-    else
-        M = sparse(proj, proj, ones(N, length(proj)), n, n)
-        return IntersectionProperty(M * prop.safe)
-    end
-end
diff --git a/src/ReachSets/Properties/IntersectionProperty.jl b/src/ReachSets/Properties/IntersectionProperty.jl
deleted file mode 100644
index 438ae2be..00000000
--- a/src/ReachSets/Properties/IntersectionProperty.jl
+++ /dev/null
@@ -1,45 +0,0 @@
-"""
-    IntersectionProperty{N<:Real} <: Property
-
-Type that represents a safety property characterized with a set of bad states.
-A safety property is satisfied by a given set of states if the intersection with
-the set of bad states is empty.
-
-### Fields
-
-- ``bad`` -- convex set representing the bad states
-- ``witness`` -- witness point (empty vector if not set)
-"""
-mutable struct IntersectionProperty{N<:Real} <: Property
-    bad::LazySet
-    witness::Vector{N}
-
-    IntersectionProperty{N}(bad::LazySet) where {N<:Real} = new(bad, N[])
-end
-
-# type-less convenience constructor
-IntersectionProperty(bad::LazySet{N}) where {N} = IntersectionProperty{N}(bad)
-
-"""
-    check_property(set::LazySet, prop::IntersectionProperty)::Bool
-
-Checks whether a convex set satisfies a safety property.
-
-### Input
-
-- ``set``  -- convex set
-- ``prop`` -- safety property with bad states
-
-### Output
-
-`true` iff the safety property is satisfied for the given set of states.
-This is the case iff the set of states does not intersect with the bad states.
-"""
-@inline function check_property(set::LazySet, prop::IntersectionProperty)::Bool
-    nonempty_intersection, witness = is_intersection_empty(set, prop.bad, true)
-    if nonempty_intersection
-        # store violation witness
-        prop.witness = witness
-    end
-    return !nonempty_intersection
-end
diff --git a/src/ReachSets/Properties/LinearConstraintProperty.jl b/src/ReachSets/Properties/LinearConstraintProperty.jl
deleted file mode 100644
index c2adc041..00000000
--- a/src/ReachSets/Properties/LinearConstraintProperty.jl
+++ /dev/null
@@ -1,72 +0,0 @@
-"""
-    Clause{N<:Real}
-
-Type that represents a disjunction of linear constraints.
-
-### Fields
-
-- ``atoms`` -- a vector of linear constraints
-"""
-struct Clause{N<:Real}
-    atoms::AbstractVector{LinearConstraint{N}}
-end
-# constructor from a single atom
-Clause(atom::LinearConstraint{N}) where {N<:Real} = Clause{N}([atom])
-
-"""
-    LinearConstraintProperty{N<:Real} <: Property
-
-Type that represents a property consisting of a Boolean function of linear
-constraints.
-The function is given in CNF (conjunctive normal form), i.e., a conjunction of
-disjunctions of linear constraints.
-
-### Fields
-
-- ``clauses`` -- a vector of `Clause` objects
-"""
-struct LinearConstraintProperty{N<:Real} <: Property
-    clauses::AbstractVector{Clause{N}}
-end
-# constructor from a single clause
-LinearConstraintProperty(clause::Clause{N}) where {N<:Real} =
-    LinearConstraintProperty{N}([clause])
-# constructor from a single constraint
-LinearConstraintProperty(linConst::LinearConstraint{N}) where {N<:Real} =
-    LinearConstraintProperty{N}([Clause(linConst)])
-# constructor from a single constraint in raw form ax+b
-LinearConstraintProperty(linComb::AbstractVector{N}, bound::N) where {N<:Real} =
-    LinearConstraintProperty{N}([Clause(LinearConstraint{N}(linComb, bound))])
-
-"""
-    check_property(set::LazySet, prop::LinearConstraintProperty)::Bool
-
-Checks whether a convex set satisfies a property of linear constraints.
-
-### Input
-
-- ``set``  -- convex set
-- ``prop`` -- property of linear constraints
-
-### Output
-
-`true` iff the convex set satisfies the property of linear constraints.
-"""
-@inline function check_property(set::LazySet, prop::LinearConstraintProperty
-                               )::Bool
-    @assert (length(prop.clauses) > 0) "empty properties are not allowed"
-    for clause in prop.clauses
-        @assert (length(clause.atoms) > 0) "empty clauses are not allowed"
-        clause_sat = false
-        for atom in clause.atoms
-            if ρ(atom.a, set) < atom.b
-                clause_sat = true
-                break
-            end
-        end
-        if !clause_sat
-            return false
-        end
-    end
-    return true
-end
diff --git a/src/ReachSets/Properties/Property.jl b/src/ReachSets/Properties/Property.jl
deleted file mode 100644
index 1d50040b..00000000
--- a/src/ReachSets/Properties/Property.jl
+++ /dev/null
@@ -1,9 +0,0 @@
-"""
-Abstract supertype of properties that can be checked.
-
-Every concrete subtype should provide the following functions:
-  - `inout_map_property(::Property, ::AbstractVector{<:AbstractVector{Int}},
-                        ::AbstractVector{Int}, ::Int)::Property`
-  - `check_property(::LazySet, ::Property)::Bool`
-"""
-abstract type Property end
diff --git a/src/ReachSets/Properties/SubsetProperty.jl b/src/ReachSets/Properties/SubsetProperty.jl
deleted file mode 100644
index 88c84d49..00000000
--- a/src/ReachSets/Properties/SubsetProperty.jl
+++ /dev/null
@@ -1,45 +0,0 @@
-"""
-    SubsetProperty{N<:Real} <: Property
-
-Type that represents a safety property characterized with a set of safe states.
-A safety property is satisfied by a given set of states if the set of states is
-fully contained in the set of safe states.
-
-### Fields
-
-- ``safe`` -- convex set representing the safe states
-- ``witness`` -- witness point (empty vector if not set)
-"""
-mutable struct SubsetProperty{N<:Real} <: Property
-    safe::LazySet
-    witness::Vector{N}
-
-    SubsetProperty{N}(safe::LazySet) where {N<:Real} = new(safe, N[])
-end
-
-# type-less convenience constructor
-SubsetProperty(safe::LazySet{N}) where {N} = SubsetProperty{N}(safe)
-
-"""
-    check_property(set::LazySet, prop::SubsetProperty)::Bool
-
-Checks whether a convex set satisfies a safety property.
-
-### Input
-
-- ``set``  -- convex set
-- ``prop`` -- safety property with safe states
-
-### Output
-
-`true` iff the safety property is satisfied for the given set of states.
-This is the case iff the set of states is a subset of the safe states.
-"""
-@inline function check_property(set::LazySet, prop::SubsetProperty)::Bool
-    is_subset, witness = ⊆(set, prop.safe, true)
-    if !is_subset
-        # store violation witness
-        prop.witness = witness
-    end
-    return is_subset
-end
diff --git a/src/ReachSets/ReachSets.jl b/src/ReachSets/ReachSets.jl
index c5596d61..d937e411 100644
--- a/src/ReachSets/ReachSets.jl
+++ b/src/ReachSets/ReachSets.jl
@@ -80,9 +80,9 @@ AUTHORS:
 """
 module ReachSets
 
-using ..Utils
-using LazySets, MathematicalSystems, HybridSystems
-using Expokit, Optim, ProgressMeter
+using ..Utils, ..Properties
+using LazySets, MathematicalSystems, HybridSystems, Expokit, Optim,
+      ProgressMeter
 
 # fix namespace conflicts with MathematicalSystems
 using LazySets: LinearMap
@@ -107,27 +107,10 @@ include("discretize.jl")
 
 export discretize
 
-# ==============================
-# Property struct and evaluation
-# ==============================
-include("Properties/Property.jl")
-export Property,
-       inout_map_property
-
-include("Properties/LinearConstraintProperty.jl")
-export LinearConstraintProperty,
-       Clause
-
-include("Properties/IntersectionProperty.jl")
-export IntersectionProperty
-
-include("Properties/SubsetProperty.jl")
-export SubsetProperty
-
 # ==========================
 # Property checking results
 # ==========================
-include("Properties/CheckSolution.jl")
+include("CheckSolution.jl")
 
 export CheckSolution
 
@@ -153,7 +136,7 @@ export available_algorithms_check,
 # ====================================================
 # Algorithms to find a threshold for property checking
 # ====================================================
-include("Properties/tune.jl")
+include("tune.jl")
 export tune_δ
 
 # =====================
diff --git a/src/ReachSets/Properties/tune.jl b/src/ReachSets/tune.jl
similarity index 100%
rename from src/ReachSets/Properties/tune.jl
rename to src/ReachSets/tune.jl
diff --git a/src/Reachability.jl b/src/Reachability.jl
index 42b40565..08ae9dd2 100644
--- a/src/Reachability.jl
+++ b/src/Reachability.jl
@@ -16,17 +16,16 @@ include("Utils/Utils.jl")
 include("Options/dictionary.jl")
 include("Options/validation.jl")
 include("Options/default_options.jl")
+include("Properties/Properties.jl")
 include("ReachSets/ReachSets.jl")
 include("Transformations/Transformations.jl")
 
 @reexport using Reachability.Utils,
                 Reachability.ReachSets,
+                Reachability.Properties,
                 Reachability.Transformations
 
 export project,
-       LinearConstraintProperty, Clause,
-       IntersectionProperty,
-       SubsetProperty,
        Transformations
 
 include("solve.jl")
diff --git a/test/Properties/unit_Property.jl b/test/Properties/unit_Property.jl
index 6c56f2a0..2c4f1478 100644
--- a/test/Properties/unit_Property.jl
+++ b/test/Properties/unit_Property.jl
@@ -1,24 +1,14 @@
-# ====================
-# Test Clause creation
-# ====================
-lc = LinearConstraint([1.; zeros(7)], 0.35)
-# vector of atoms
-c1 = Clause([lc, LinearConstraint([zeros(4); 1.; zeros(3)], 0.45)])
-# single atom
-c2 = Clause(lc)
-
 # ======================
-# Test LinearConstraintProperty creation
+# Test property creation
 # ======================
-# vector of clauses
-p1 = LinearConstraintProperty([c1, c2])
-# single clause
-p2 = LinearConstraintProperty(c1)
-# single constraint
-p3 = LinearConstraintProperty(lc)
-# single raw constraint
-p4 = LinearConstraintProperty([1.; zeros(7)], 0.35)
+X1 = LinearConstraint([1.; zeros(7)], 0.35)
+X2 = LinearConstraint([zeros(4); 1.; zeros(3)], 0.45)
 
+p1 = SafeStatesProperty(X1)
+p2 = BadStatesProperty(X2)
+p3 = Conjunction([p1, p2])
+p4 = Disjunction([p1, p2])
+p5 = Conjunction([p3, Disjunction([p1, p4]), p2])
 
 # just have one actual test case...
 @test true
diff --git a/test/Properties/unit_tune.jl b/test/Properties/unit_tune.jl
index 52f430c8..f53a3465 100644
--- a/test/Properties/unit_tune.jl
+++ b/test/Properties/unit_tune.jl
@@ -1,4 +1,4 @@
-using Reachability.ReachSets: BFFPSV18
+using Reachability.ReachSets: tune_δ
 
 #===== Projectile model =====
 We test the line plot!(x->x, x->-24*x+375, 0., 50., line=2., color="red", linestyle=:solid, legend=:none)
@@ -10,11 +10,12 @@ S = ContinuousSystem(A, X0, U)
 time_horizon = 20.0
 prec = 1e-4
 initial_δ = 0.5
+property = SafeStatesProperty(LinearConstraint([24., 0., 1, 0], 375.))
 algorithm(N, δ) =
     solve(S,
           Options(:mode => "check", :plot_vars => [1, 3], :T => time_horizon,
-                  :property=>LinearConstraintProperty([24., 0., 1, 0],  375.));
+                  :property => property),
           op=BFFPSV18(:δ => δ, :vars => [1, 3], :partition=>[1:2, 3:4])
          ).satisfied
 
-Reachability.tune_δ(algorithm, time_horizon, prec, initial_δ)
+tune_δ(algorithm, time_horizon, prec, initial_δ)
diff --git a/test/ReachSets/unit_discretization.jl b/test/ReachSets/unit_discretization.jl
index 3af9a9ce..77297ea4 100644
--- a/test/ReachSets/unit_discretization.jl
+++ b/test/ReachSets/unit_discretization.jl
@@ -1,5 +1,3 @@
-import Reachability.ReachSets.discretize
-
 let # preventing global scope
     # ===================================================================
     # Discretization of a continuous-time system without input (ZeroSet)
diff --git a/test/Reachability/solve_continuous.jl b/test/Reachability/solve_continuous.jl
index 258a94e4..a429ccae 100644
--- a/test/Reachability/solve_continuous.jl
+++ b/test/Reachability/solve_continuous.jl
@@ -1,9 +1,6 @@
 # ===============================
 # Test minimal (default) options
 # ===============================
-using Reachability, MathematicalSystems
-using Reachability.ReachSets: BFFPSV18
-using LinearAlgebra, SparseArrays
 
 # linear ODE: x' = Ax
 A = [ 0.0509836  0.168159  0.95246   0.33644
@@ -50,14 +47,14 @@ A = [ 0.0509836  0.168159  0.95246   0.33644
 # check that x1 + x2 <= 2 doesn't hold
 s = solve(ContinuousSystem(A, X0),
           Options(:T=>0.1, :mode=>"check",
-          :property=>LinearConstraintProperty([1., 1., 0., 0.], 2.)),
+          :property=>SafeStatesProperty(LinearConstraint([1., 1., 0., 0.], 2.))),
           op=BFFPSV18(:vars=>[1,2,3], :partition=>[1:2, 3:4]))
 @test s.violation == 1
 
 # check that x1 - x2 <= 2 holds
 s = solve(ContinuousSystem(A, X0),
           Options(:T=>0.1, :mode=>"check",
-          :property=>LinearConstraintProperty([1., -1., 0., 0.], 2.)),
+          :property=>SafeStatesProperty(LinearConstraint([1., -1., 0., 0.], 2.))),
           op=BFFPSV18(:vars=>[1,2,3], :partition=>[1:2, 3:4]))
 @test s.violation == -1
 
diff --git a/test/Systems/alltests.jl b/test/Systems/alltests.jl
index dff2dba8..c4f24919 100644
--- a/test/Systems/alltests.jl
+++ b/test/Systems/alltests.jl
@@ -1,4 +1,2 @@
-using MathematicalSystems
-
 @time @testset "Systems.NonDeterministicInput" begin include("unit_NonDeterministicInput.jl") end
 @time @testset "Systems.System" begin include("unit_System.jl") end
diff --git a/test/runtests.jl b/test/runtests.jl
index 744f8f2b..adac2556 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -1,5 +1,6 @@
 #!/usr/bin/env julia
-using LazySets, Reachability, MathematicalSystems
+using LazySets, Reachability, MathematicalSystems,
+      LinearAlgebra, SparseArrays
 
 # fix namespace conflicts with MathematicalSystems
 import LazySets.LinearMap