1 Abstract
In this article, we introduce the Contradiction Finding Unit or the CFU. Just as the ALU (Arithmetic Logic Unit) is the workhorse behind arithmetic and logic operations within general-purpose computers, the CFU is the workhorse behind the computational identification of trust impairments within the local computers used by actors within a trustworthy distributed system. The CFU is also central to the discovery and local validation of private intentions held within the distributed system, which explain one or more trust impairments identified by an actor.
This article also makes liberal use of concepts from undergraduate-level mathematics and computer science. This warning will be omitted from future articles.
2 Introduction
We start off by describing the problem of identifying trust impairments, which, as discussed in an earlier article, may also be thought of as a contradiction finding problem.
Given a context \(\mathsf{Ctx} = \{s_0, s_1, \ldots, s_{N-1}\}\) with \(N\) statements, return 1 if there exists a set of statements \(S\) containing a logical contradiction such that \(S \subseteq \mathsf{Ctx},\) and 0 otherwise.
One can think of variants of the same problem. One variant might entail returning the smallest subset \(S \subseteq \mathsf{Ctx},\) such that \(S\) contains a logical contradiction, and a null set if there are no contradictions within \(\mathsf{Ctx}\). Another variant might entail returning M non-overlapping subsets \({S_0, S_1, \ldots, S_{M-1}}\) such that \(S_i \subseteq \mathsf{Ctx}, S_i \cap S_j = \emptyset\) for all \(i,j \in \{0, 1, \ldots, M-1\}, i \neq j\) and all \(S_i\) being either the null set or one that contains a logical contradiction. For this article, we stick to the simplest variant.
The Contradiction Finding Unit (CFU) is a processing unit within a computer which solves the contradiction finding problem taking a context \(\mathsf{Ctx}\) as an input.
Different implementations of the CFU may address, in addition to the simplest variant, other variants of the contradiction finding problem. Some of these variants may be more relevant in some real-world verticals than in others. The CFU may be implemented using software (which may be run on general-purpose CPUs or GPUs), in hardware (e.g., via ASICs or using FPGAs) or via a combination of the two, leveraging programmable hardware.
3 Algorithms for contradiction finding
A brute force algorithm for finding logical contradictions within a context \(\mathsf{Ctx}\) containing \(N\) statements makes use of the following observation, where \(\mathsf{Ctx}_0\) is the null set \(\emptyset\) and \(\mathsf{Ctx}_{m}\) with \(1 \leq m \leq N\) denotes the context \(\{s_0, \ldots, s_{m-1}\}.\)
If \(\mathsf{Ctx}_{m_0}\) does not have a logical contradiction, any \(\mathsf{Ctx}_{m_1}\) with \(m_1 \leq m_0\) also does not have a logical contradiction.
Then, an algorithm exploiting the above observation is as follows. Starting with \(m = 1\), and moving sequentially up to \(m = N,\) for each \(m\):
we consider the set \(W_m = \{S\cup\{s_m\}: S \in P(\mathsf{Ctx_{m-1}})\},\) where \(P(X)\) is the power set of \(X,\) and
check to see if there exists a logical contradiction in any set \(T \in W_m\). Return 1 if a contradiction is found.
If no contradictions are found, the algorithm returns 0.
The runtime complexity of the above algorithm grows exponentially with \(N\) in the worst case. However, the logical relationships among the statements within the context and the representation of those statements within the semantics of a formal language can dramatically reduce the runtime complexity of finding contradictions. We discuss some of these speedups in later articles.
For example, a particular context may be reduced via applying carefully designed context reduction functions introduced in an earlier article to reduce a single context to multiple logically independent sub-contexts, which may be further reduced to “minimal” sub-contexts containing only the minimum possible number of logically independent statements (i.e., to logically independent sets of axioms). These context reductions can then enable parallelization-induced speedups of finding contradictions by a factor equal to the number of logically independent sets of statements. Even when strict logical independence does not hold, “weak” independence can already unlock significant parallelization-induced speedups in many practical contradiction-finding workloads, especially with processors capable of massively parallel computations such as GPUs and/or FPGAs.
Practical contradiction-finding computational workloads can also leverage randomized algorithms for significant speedups on massively parallel computation platforms. Instead of searching over all sets within the power set of the context, these algorithms sample random sets from the power set, sometimes informed by judiciously chosen heuristics.
4 Discovering private intentions using CFUs
When a logical contradiction is discovered by a local actor within a set \(S \in \mathsf{Ctx},\) resolving the contradiction may involve removing statements from \(S\) until the contradiction is removed.
However, discovery of one or more contradictions may also lead to actors adding statements to or modifying statements within \(\mathsf{Ctx}\) locally until the contradiction(s) is(are) resolved. Such additions or modifications typically need to be followed by contradiction finding to ensure that no additional contradictions have been introduced. Once logical contradictions are removed from a context, various context reduction or extension functions may be applied to the context towards discovering private intentions from statements already within the context.
5 Summary
In this article, we introduced the Contradiction Finding Unit (CFU), which detects computationally the existence of logical contradictions within a context of statements maintained locally by an actor within a trustworthy distributed system. Some preliminary algorithms for contradiction finding and the use of CFUs in discovering private intentions within trustworthy distributed systems were also discussed.
6 Changelog
This document was first published on December 3, 2025. It was last modified on December 5, 2025.
7 Feedback
The author of this article would love to hear your feedback at hello@milaneum.io. In your message, please consider including the name of the article, the listed identity of the Milaneal author of this article, and the semantic version.