# Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework
> Corresponding author: Hao Fei
## Abstract
In the context of large language models (LLMs), current advanced reasoning methods have made impressive strides in various reasoning tasks. However, when it comes to logical reasoning tasks, major challenges remain in both efficacy and efficiency. This is rooted in the fact that these systems fail to fully leverage the inherent structure of logical tasks throughout the reasoning processes such as decomposition, search, and resolution. To address this, we propose a logic-complete reasoning framework, Aristotle, with three key components: Logical Decomposer, Logical Search Router, and Logical Resolver. In our framework, symbolic expressions and logical rules are comprehensively integrated into the entire reasoning process, significantly alleviating the bottlenecks of logical reasoning, i.e., reducing sub-task complexity, minimizing search errors, and resolving logical contradictions. The experimental results on several datasets demonstrate that Aristotle consistently outperforms state-of-the-art reasoning frameworks in both accuracy and efficiency, particularly excelling in complex logical reasoning scenarios. We will open-source all our code at http://llm-symbol.github.io/Aristotle.
## 1 Introduction
LLMs Patel et al. (2023); Chowdhery et al. (2023) have unlocked unprecedented potential in semantic understanding Zhao et al. (2023), sparking immense hope for realizing AGI. A fundamental requirement for true intelligence is the ability to perform human-level reasoning, such as commonsense reasoning Wang et al. (2024c), mathematical problem-solving Wang et al. (2024a), and geometric reasoning Eisner et al. (2024). To achieve this, researchers have drawn inspiration from human reasoning processes, proposing various methods and strategies for LLM-based reasoning. One of the most groundbreaking works is the Chain-of-Thought (CoT) Wei et al. (2022), which breaks down complex problems into smaller sub-problems, solving them step by step. The birth of CoT has elevated the reasoning capabilities of LLMs to new heights. Further research has built on this foundation by closely emulating human cognitive patterns, introducing more advanced approaches, such as Least-to-Most Zhou et al. (2023), Tree-of-Thought (ToT) Yao et al. (2023), Graph-of-Thought (GoT) Besta et al. (2024), and Plan-and-Solve Wang et al. (2023a), which have achieved progressively better results on reasoning benchmarks. In summary, successful LLM-based reasoning methods generally involve three key modules Huang and Chang (2023); Li et al. (2024): problem decomposition, path searching, and problem resolution.
<details>
<summary>x1.png Details</summary>
### Visual Description
\n
## Bar Chart: Error Rate and Reasoning Steps Comparison
### Overview
This image presents a comparative bar chart illustrating the performance of two methods, "ToT" (Tree of Thoughts) and "Ours," across two evaluation metrics: Error Rate (%) and Reasoning Steps. The chart consists of two sub-charts, side-by-side, each comparing the two methods on one metric. The chart uses a color scheme of blue for "ToT" and red for "Ours". Red arrows indicate the percentage difference between the two methods.
### Components/Axes
* **X-axis (Both Charts):** Categories representing the evaluation tasks: "SE" (likely representing a task type) and "RE" (likely representing another task type).
* **Y-axis (Left Chart):** Error Rate (%), ranging from 0 to 30.
* **Y-axis (Right Chart):** Reasoning Steps, ranging from 0 to 30.
* **Legend (Top-Left):**
* Blue: "ToT"
* Red: "Ours"
* **Arrows:** Red arrows with percentage values indicating the difference in performance between "ToT" and "Ours".
### Detailed Analysis or Content Details
**Left Chart: Error Rate (%)**
* **SE:**
* ToT (Blue): Approximately 15.0%. The bar reaches the 15% mark on the y-axis.
* Ours (Red): Approximately -11.1%. The bar reaches the -11.1% mark on the y-axis.
* Difference (Arrow): -28.0% (indicating "Ours" has a 28% lower error rate than "ToT").
* **RE:**
* ToT (Blue): Approximately 28.4%. The bar reaches the 28.4% mark on the y-axis.
* Ours (Red): Approximately 0%. The bar is very short, close to the x-axis.
* Difference (Arrow): -28.0% (indicating "Ours" has a 28% lower error rate than "ToT").
**Right Chart: Reasoning Steps**
* **SE:**
* ToT (Blue): Approximately 24.6. The bar reaches the 24.6 mark on the y-axis.
* Ours (Red): Approximately 11.7. The bar reaches the 11.7 mark on the y-axis.
* Difference (Arrow): -12.9 (indicating "Ours" requires 12.9 fewer reasoning steps than "ToT").
* **RE:**
* ToT (Blue): Approximately 24.6. The bar reaches the 24.6 mark on the y-axis.
* Ours (Red): Approximately 11.7. The bar reaches the 11.7 mark on the y-axis.
* Difference (Arrow): -12.9 (indicating "Ours" requires 12.9 fewer reasoning steps than "ToT").
### Key Observations
* "Ours" consistently outperforms "ToT" in both Error Rate and Reasoning Steps across both tasks (SE and RE).
* The reduction in Error Rate is substantial, particularly for the "RE" task, where "Ours" achieves an error rate close to zero.
* The reduction in Reasoning Steps is consistent across both tasks, approximately 12.9 steps.
* The error rate for "ToT" is significantly higher for the "RE" task compared to the "SE" task.
### Interpretation
The data suggests that the "Ours" method is significantly more efficient and accurate than the "ToT" method for both "SE" and "RE" tasks. The substantial reduction in error rate, especially for the "RE" task, indicates that "Ours" is better at avoiding mistakes. The lower number of reasoning steps suggests that "Ours" is more streamlined and requires less computational effort. The consistent performance improvement across both tasks implies that the benefits of "Ours" are not task-specific. The large difference in error rate between the two tasks for "ToT" suggests that "ToT" may struggle with the complexities of the "RE" task. The arrows clearly highlight the magnitude of the improvement offered by "Ours" in both metrics.
</details>
Figure 1: Our reasoning framework vs. the SoTA ToT: comparison in terms of Search Error (SE) and single-step Reasoning Error (RE), as well as in terms of average number of reasoning steps.
<details>
<summary>x2.png Details</summary>
### Visual Description
\n
## Diagram: Reasoning Trajectories for Knowledge Representation
### Overview
This diagram illustrates a three-step process for answering a question based on a given premise using a reasoning system. The process involves translating and decomposing the premise and question, searching for complementary clauses, and concluding with an answer. The diagram depicts the flow of information and the reasoning trajectories involved in this process.
### Components/Axes
The diagram is divided into three main steps: Step 1: Search Initialization, Step 2: Search and Resolve, and Step 3: Conclude Answer. Each step contains several components, including:
* **Raw Input:** Contains the premise (P) and question (S).
* **Translator:** Converts the input into a suitable format.
* **Decomposer:** Breaks down the premise and question into smaller clauses.
* **Premises (Pn):** The decomposed premise.
* **Question (Sn):** The decomposed question.
* **Resolver:** Identifies contradictions and resolves clauses.
* **Search Router:** Guides the search for complementary clauses.
* **Reasoning Complete?:** A decision point indicating whether the reasoning process is finished.
* **Proof:** Indicates whether a contradiction or no contradiction was found.
* **Current Clause:** The clause being currently evaluated.
* **Complementary Clause:** A clause that complements the current clause.
* **Resolved Clause:** The result of resolving the current and complementary clauses.
* **Final Answer:** The answer to the question.
The diagram also includes labels for the input, intermediate steps, and output.
### Detailed Analysis or Content Details
**Step 1: Search Initialization**
* **Raw Input:**
* Premise (P): "If people are patient, then they are nice. If people are smart, then they patient. Dave is smart."
* Question (S): "Dave is nice."
* (True/False/Unknown) Self-Contradiction
* **Translator & Decomposer:** These components transform the raw input.
* **Translated & Decomposed Premises (Pn):**
1. Patient(x, False) v Nice(x, True)
2. Smart(x, False) v Patient(x, True)
3. Smart(Dave, True)
* **Question (Sn):** Nice(Dave, True)
* **Initialization:** Sn: Nice(Dave, True) and ~Sn: Nice(Dave, False)
**Step 2: Search and Resolve**
* **Current Clause:** ~Sn: Nice(Dave, False)
* **Premises (Pn):** 1, 2, 3 (as listed above)
* **Search Router:** Guides the search for complementary clauses.
* **Complementary Clause:** Patient(x, False) v Nice(x, True)
* **No Complementary Clause found.**
**Step 3: Conclude Answer**
* **Reasoning Complete?:** No -> Yes
* **Reasoning Trajectories (Right Side of Diagram):** This section shows multiple reasoning paths.
* **Round 2:**
* Current Clause: ~Sn: Nice(Dave, False)
* Complementary Clause: Patient(x, False) v Nice(x, True)
* Resolved Clause: Patient(Dave, False)
* Start 2nd round
* **Round 3:**
* Current Clause: Smart(Dave, False)
* Complementary Clause: Smart(x, False) v Patient(x, True)
* Resolved Clause: Contradiction!
* D<sub>s</sub> = P<sub>n</sub> + S<sub>n</sub>
* **Final Round:**
* Current Clause: Sn: Nice(Dave, True)
* Complementary Clause: No complementary clause found.
* Resolved Clause: No Contradiction
* D<sub>s</sub> = P<sub>n</sub> +/~S<sub>n</sub>
* **Final Answer:** The answer is True.
**Resolved Clause Boxes (Orange):** These boxes show the result of resolving clauses.
### Key Observations
The diagram demonstrates a logical reasoning process. The reasoning trajectories show how the system explores different paths to arrive at an answer. The presence of "Contradiction!" in one trajectory suggests that the system can identify inconsistencies. The final answer being "True" indicates that the premise supports the question.
### Interpretation
The diagram illustrates a knowledge representation and reasoning system. The system takes a premise and a question as input, decomposes them into logical clauses, and searches for complementary clauses to resolve contradictions. The reasoning trajectories show the different paths the system can take to arrive at an answer. The system's ability to identify contradictions and provide a final answer suggests that it is capable of performing logical inference. The diagram highlights the importance of decomposing complex statements into smaller, manageable clauses for effective reasoning. The use of "D<sub>s</sub>" suggests a formal representation of the derived statement based on the premise and question. The diagram is a visual representation of a formal logic process, likely used in artificial intelligence or knowledge-based systems.
</details>
Figure 2: Our Aristotle logical reasoning framework (best viewed via zooming in). In step 1, the
<details>
<summary>figure/translation.png Details</summary>
### Visual Description
\n
## Icon: Language Translation
### Overview
The image is a flat-style icon representing language translation. It depicts two overlapping rectangular shapes, one light blue and one white, with arrows indicating a bidirectional flow between the characters "文" (Chinese/Japanese) and "A" (English).
### Components/Axes
There are no axes or scales present in this icon. The key components are:
* **Character "文"**: Located in the upper-left quadrant, within the white rectangle.
* **Character "A"**: Located in the lower-right quadrant, within the light blue rectangle.
* **Arrows**: Two curved arrows, one pointing from "文" to "A" (top-right) and the other from "A" to "文" (bottom-left).
* **Rectangles**: Overlapping light blue and white rectangles.
### Detailed Analysis or Content Details
The icon visually represents the concept of translation between two languages. The character "文" is a Chinese or Japanese character meaning "text" or "language". The character "A" represents the English alphabet. The arrows indicate a two-way translation process.
* **"文" (wén)**: This is a Chinese character (and also used in Japanese). Its English translation is "text", "language", "literature", or "pattern".
* **"A"**: The first letter of the English alphabet.
### Key Observations
The icon is simple and direct in its representation of language translation. The overlapping rectangles suggest the interconnectedness of languages. The arrows clearly indicate the bidirectional nature of the translation process.
### Interpretation
This icon is a visual metaphor for language translation services or tools. It suggests the ability to convert text from one language to another and vice versa. The use of a single character from an East Asian language and a single letter from the English alphabet emphasizes the broad scope of translation possibilities. The icon is likely used in applications or websites related to translation, localization, or language learning. It does not contain any factual data or numerical values, but rather conveys a conceptual idea.
</details>
Translator and
<details>
<summary>figure/decomposer.png Details</summary>
### Visual Description
\n
## Diagram: Hierarchical Structure
### Overview
The image depicts a hierarchical diagram, resembling a tree structure or organizational chart. It consists of interconnected rectangular boxes of varying colors, linked by blue lines representing relationships or flow. There are no labels or numerical data present within the diagram itself. The diagram is centered on a light gray background.
### Components/Axes
The diagram is composed of:
* **Root Node:** A single, large, yellow rectangular box at the top-center.
* **Level 1 Nodes:** Two rectangular boxes branching from the root node: a red box on the left and a teal box on the right.
* **Level 2 Nodes:** Three rectangular boxes branching from the Level 1 nodes: a green box branching from the red box, a yellow box branching from the red box, and a blue box branching from the teal box.
There are no axes, scales, or legends explicitly present in the image. The colors of the boxes appear to be purely for visual differentiation.
### Detailed Analysis or Content Details
The diagram shows a branching structure. The root node connects to two nodes at the next level, and these nodes further connect to three nodes at the lowest level.
* **Root Node:** Yellow
* **Level 1 - Left Branch:** Red
* **Level 1 - Right Branch:** Teal
* **Level 2 - From Red:** Green, Yellow
* **Level 2 - From Teal:** Blue
The lines connecting the boxes are all blue and appear to indicate a parent-child relationship or a flow of information. The diagram is symmetrical in terms of branching, with the root node splitting into two branches, and the red branch splitting into two further branches.
### Key Observations
The diagram illustrates a hierarchical relationship. The structure suggests a top-down flow or organization. The lack of labels makes it impossible to determine the specific meaning of the hierarchy. The color coding is arbitrary without a legend.
### Interpretation
The diagram represents a basic hierarchical structure. It could depict an organizational chart, a decision tree, a family tree, or any other system where elements are organized in a parent-child relationship. The absence of labels means the diagram is purely structural and doesn't convey specific information about the entities it represents. The diagram suggests a relatively simple hierarchy with a single root and a limited number of levels. The symmetry of the branching might indicate a balanced or evenly distributed structure. Without further context, it's difficult to determine the specific purpose or meaning of the diagram. It is a visual representation of relationships, but lacks the data to provide deeper insights.
</details>
Decomposer together transform $P$ and $S$ into $P_{n}$ and $S_{n}$ . Then, we initialize the $C_{\text{current}}$ using the decomposed $S_{n}$ and $\neg S_{n}$ . In step 2, the
<details>
<summary>x5.png Details</summary>
### Visual Description
Icon/Small Image (29x29)
</details>
Search Router uses the $C_{\text{current}}$ and $P_{n}$ to search for $C_{\text{complement}}$ . The
<details>
<summary>x6.png Details</summary>
### Visual Description
Icon/Small Image (29x29)
</details>
Resolver then resolves $C_{\text{current}}$ with $C_{\text{complement}}$ to produce $C_{\text{resolved}}$ . The reasoning complete if: (1) the $C_{\text{resolved}}$ determines whether a contradiction exists; (2) reach the maximum number of iterations $I_{\text{max}}$ . In step 3, Aristotle then concludes the Proof $D_{S_{n}}$ and $D_{\neg S_{n}}$ based on the Proof Determination. Using these proofs, Aristotle determines the final answer based on Eq. (1). Note that two distinct reasoning paths will be implemented: a solid box representing the path starting from $\neg S_{n}$ , and a dotted box representing the path starting from $S_{n}$ . The complete reasoning process for both two paths, including all iterations are shown in the right part “ Reasoning Trajectories ”.
Compared to other forms of general reasoning, logical reasoning Huang and Chang (2023) stands out as one of the most challenging tasks, as it demands the strictest evidence, arguments, and logical rigor to arrive at sound conclusions or judgments. Logical reasoning more closely mirrors human-level cognitive processes, making it crucial in high-stakes domains such as mathematical proof generation, legal analysis, and scientific discovery Cummins et al. (1991); Markovits and Vachon (1989). In recent years, numerous studies have investigated how to integrate LLMs into logical reasoning. For example, some methods Pan et al. (2023); Gao et al. (2023) use LLMs to translate textual problems into symbolic expressions, which are then addressed by external logic solvers. Subsequent work, such as SymbCoT Xu et al. (2024), suggests that LLMs themselves can handle both symbolic translation and logic resolution, thus avoiding potential information loss caused when using external solvers. While SymbCoT has achieved state-of-the-art (SoTA) performance, the inherent simplicity of CoT’s linear reasoning process leaves considerable room for further improvement in LLM-based logical reasoning.
In response, certain research Yao et al. (2023); Besta et al. (2024); Zhang et al. (2023) has applied sophisticated general-purpose reasoning methods (e.g., ToT, GoT) directly to logical reasoning tasks. Unfortunately, these approaches largely overlook the inherent structure of logical tasks and fail to effectively integrate logical rules into the decompose-search-resolve framework, leaving key issues unresolved in both reasoning efficacy and efficiency:
$\blacktriangleright$ From an efficacy perspective, first, when LLMs decompose logical problems, they often rely on the linguistic token relations rather than the underlying logical structure, leading to disconnected sub-problems and faulty reasoning. Specifically, when reasoning hinges on specific logical relationships, neglecting them can result in disjointed sub-problems, breaking the logical chain and ultimately leading to incorrect conclusions. Furthermore, during the search stage, current path search methods rely heavily on evaluators that may be unreliable, selecting nodes based on possibly flawed logic, causing error propagation through subsequent reasoning steps Chen et al. (2024); Wang et al. (2024b). For the resolving step, these methods guide LLMs to solve sub-questions with simple text prompts, which frequently contain logical errors, resulting in numerous faulty nodes in the search space Xu et al. (2024). These errors propagate through subsequent reasoning steps, causing entire paths to fail and leading to reasoning failure. Our preliminary experiments reveal that directly applying SoTA general-purpose reasoning methods with a search mechanism to logical tasks results in significant errors, with 28.4% for reasoning and 15.0% for search, as shown in Fig. 1.
$\blacktriangleright$ From an efficiency perspective, these approaches also lead to significant shortcomings. For example, generating large numbers of incorrect nodes wastes computational resources Ning et al. (2024). Moreover, relying on unreliable evaluators introduces bias into the search process, leading to unnecessary node and path explorations, ultimately reducing efficiency Chen et al. (2024). We note that inefficient logical reasoning systems can significantly undermine their value in practical application scenarios.
To address these challenges, we propose a novel reasoning framework, Aristotle, which effectively tackles the performance and the efficiency bottlenecks in existing logical reasoning tasks by completely integrating symbolic expressions and rules into each stage of the decomposition, search, and resolution. Fig. 2 illustrates the overall framework. Specifically, we first introduce a Logical Decomposer that breaks down the original problem into smaller and simpler components based on its logical structure, reducing the complexity of logical tasks. We then devise a Logical Search Router, which leverages proof by contradiction to directly search for logical inconsistencies, thereby reducing search errors from unreliable evaluators and minimizing the number of steps required by existing methods. Finally, we develop a Logical Resolver, which rigorously resolves logical contradictions at each reasoning step, guided by the Logical Search Router. Overall, Aristotle thoroughly considers the inherent logical structure of tasks, fully incorporating logical symbols into the entire decompose-search-resolve framework. This ensures a more logically coherent reasoning process, leading to more reliable final results.
We conducted experiments across multiple logical reasoning benchmarks, where our method surpasses the current SoTA baselines by 4.5% with GPT-4 and 5.4% with GPT-4o. Further analysis revealed that the decomposer, search router, and resolver modules each contributed to: (i) reducing task complexity during problem decomposition, leading to improved accuracy in subsequent search and reasoning phases; (ii) focusing search efforts on the most direct and relevant paths, which reduced errors and enhanced efficiency; (iii) achieving near-perfect logical reasoning accuracy. Moreover, we observe that Aristotle delivers even greater performance improvements in complex scenarios, such as those with more intricate logical structures or longer reasoning chains. Overall, this work marks the first successful complete integration of symbolic logic expressions into every stage of an LLM-based reasoning framework (decomposition, search, and resolution), demonstrating that LLMs can perform complete logical reasoning over symbolic structures.
## 2
<details>
<summary>figure/aristotle_icon.png Details</summary>
### Visual Description
\n
## Icon: Elderly Man
### Overview
The image depicts a stylized, cartoon-like icon of an elderly man. It is a simple illustration with bold outlines and flat colors. There is no quantitative data or axes present. This is a visual representation, not a data-driven chart or diagram.
### Components/Axes
There are no axes, scales, or legends present in this image. The image consists solely of the icon itself.
### Detailed Analysis or Content Details
The icon features:
* **Head:** A roughly circular head shape with gray hair. The hair is depicted with a wavy pattern.
* **Face:** A skin tone of light orange. The eyes are simple, dark brown ovals. The eyebrows are dark brown and slightly arched.
* **Beard:** A full beard, colored gray, covering the lower portion of the face.
* **Clothing:** A draped garment, colored a pale peach, covering the shoulders and upper chest.
* **Outline:** A thick black outline defines the entire figure.
### Key Observations
The style is consistent throughout the icon, suggesting a unified design. The color palette is limited, using primarily gray, orange, and peach. The overall impression is one of wisdom and age.
### Interpretation
This icon likely represents an elderly man, possibly a sage, philosopher, or historical figure. The simplicity of the design suggests it is intended for use in a user interface, as a symbol, or as a visual element in a larger composition. The lack of specific details allows for broad interpretation. The icon does not convey any specific data or trends; it is purely a symbolic representation. It is a visual shorthand for the concept of an older male.
</details>
Aristotle Architecture
We first formally define the logical reasoning task. Given a set of premises $P=\{p_{1},p_{2},\ldots,p_{n}\}$ , where each $p_{i}$ represents a logical statement, a reasoner should derive an answer $A$ regarding a given statement $S$ . The possible answer is true ( $T$ ), false ( $F$ ), unknown ( $U$ ), or self-contradictory ( $SD$ ). Self-contradictory means a statement can be proved true and false simultaneously. The formal definition of each answer can be found in Eq. (1).
As illustrated in Fig. 2, Aristotle has an architecture with four modules: Translator, Decomposer, Search Router, and Resolver.
####
<details>
<summary>figure/translation.png Details</summary>
### Visual Description
\n
## Icon: Language Translation
### Overview
The image is a flat-style icon representing language translation. It depicts two overlapping rectangular shapes, one light blue and one white, with arrows indicating a bidirectional flow between the characters "文" (Chinese/Japanese) and "A" (English).
### Components/Axes
There are no axes or scales present in this icon. The key components are:
* **Character "文"**: Located in the upper-left quadrant, within the white rectangle.
* **Character "A"**: Located in the lower-right quadrant, within the light blue rectangle.
* **Arrows**: Two curved arrows, one pointing from "文" to "A" (top-right) and the other from "A" to "文" (bottom-left).
* **Rectangles**: Overlapping light blue and white rectangles.
### Detailed Analysis or Content Details
The icon visually represents the concept of translation between two languages. The character "文" is a Chinese or Japanese character meaning "text" or "language". The character "A" represents the English alphabet. The arrows indicate a two-way translation process.
* **"文" (wén)**: This is a Chinese character (and also used in Japanese). Its English translation is "text", "language", "literature", or "pattern".
* **"A"**: The first letter of the English alphabet.
### Key Observations
The icon is simple and direct in its representation of language translation. The overlapping rectangles suggest the interconnectedness of languages. The arrows clearly indicate the bidirectional nature of the translation process.
### Interpretation
This icon is a visual metaphor for language translation services or tools. It suggests the ability to convert text from one language to another and vice versa. The use of a single character from an East Asian language and a single letter from the English alphabet emphasizes the broad scope of translation possibilities. The icon is likely used in applications or websites related to translation, localization, or language learning. It does not contain any factual data or numerical values, but rather conveys a conceptual idea.
</details>
Translator.
We use the LLM itself to parse the given premises $P$ and question statement $S$ into a symbolic format, which aims to eliminate ambiguity and ensure precision in the logical statement. We specifically use Logic Programming (LP) language, adopting Prolog’s grammar Clocksin and Mellish (2003) to represent the problem as facts, rules, and queries. Facts and rules Baader et al. (2003) are derived from $P$ , while queries are formulated based on the $S$ . We denote the translated premises (facts and rules) as $P_{t}$ , and queries as $S_{t}$ . The details of the grammar can be found at A
####
<details>
<summary>figure/decomposer.png Details</summary>
### Visual Description
\n
## Diagram: Hierarchical Structure
### Overview
The image depicts a hierarchical diagram, resembling a tree structure or organizational chart. It consists of interconnected rectangular boxes of varying colors, linked by blue lines representing relationships or flow. There are no labels or numerical data present within the diagram itself. The diagram is centered on a light gray background.
### Components/Axes
The diagram is composed of:
* **Root Node:** A single, large, yellow rectangular box at the top-center.
* **Level 1 Nodes:** Two rectangular boxes branching from the root node: a red box on the left and a teal box on the right.
* **Level 2 Nodes:** Three rectangular boxes branching from the Level 1 nodes: a green box branching from the red box, a yellow box branching from the red box, and a blue box branching from the teal box.
There are no axes, scales, or legends explicitly present in the image. The colors of the boxes appear to be purely for visual differentiation.
### Detailed Analysis or Content Details
The diagram shows a branching structure. The root node connects to two nodes at the next level, and these nodes further connect to three nodes at the lowest level.
* **Root Node:** Yellow
* **Level 1 - Left Branch:** Red
* **Level 1 - Right Branch:** Teal
* **Level 2 - From Red:** Green, Yellow
* **Level 2 - From Teal:** Blue
The lines connecting the boxes are all blue and appear to indicate a parent-child relationship or a flow of information. The diagram is symmetrical in terms of branching, with the root node splitting into two branches, and the red branch splitting into two further branches.
### Key Observations
The diagram illustrates a hierarchical relationship. The structure suggests a top-down flow or organization. The lack of labels makes it impossible to determine the specific meaning of the hierarchy. The color coding is arbitrary without a legend.
### Interpretation
The diagram represents a basic hierarchical structure. It could depict an organizational chart, a decision tree, a family tree, or any other system where elements are organized in a parent-child relationship. The absence of labels means the diagram is purely structural and doesn't convey specific information about the entities it represents. The diagram suggests a relatively simple hierarchy with a single root and a limited number of levels. The symmetry of the branching might indicate a balanced or evenly distributed structure. Without further context, it's difficult to determine the specific purpose or meaning of the diagram. It is a visual representation of relationships, but lacks the data to provide deeper insights.
</details>
Decomposer.
By breaking down the logical statement into a standardized logical form, we can simplify the reasoning process, making it easier to apply formal rules and perform efficient logical calculations. To achieve this, we use an LLM to transform the parsed premises $P_{t}$ , and queries $S_{t}$ into a standardized logical form through Normalization Davis and Putnam (1960) and Skolemization Nonnengart (1996), converting them into Conjunctive Normal Form (CNF) and eliminates quantifiers, denoted as $P_{n}$ and $S_{n}$ . For example, the logical rule $\forall x\,(P(x)\rightarrow Q(x))$ will be decomposed into $\neg P(x)\lor Q(x)$ .
####
<details>
<summary>x7.png Details</summary>
### Visual Description
Icon/Small Image (29x29)
</details>
Search Router.
We adopt the proof-by-contradiction Bishop (1967) approach because it allows us to straightforwardly search for complementary clauses. This method reduces search errors and directly targets logical conflicts, making the reasoning process faster and more efficient. We design a rule-based module to search for the clauses $C_{\text{complement}}\in P_{n}$ such that $C_{\text{current}}$ and $C_{\text{complement}}$ contain complementary terms. Terms are complementary when they share the same predicate and argument, but have opposite polarity. For example, if the $C_{\text{current}}$ is $\text{P}(\text{x},\text{True})$ , clauses in the premises that contains $\text{P}(\text{x},\text{False})$ will be found by the Search Router as $C_{\text{complement}}$ , since they are complementary (same predicate $P$ and argument $x$ but opposite polarity (True vs. False)). We will explain how we define the $C_{\text{current}}$ in Section 3. We include more details about the search strategy in Appendix B and H.
####
<details>
<summary>x8.png Details</summary>
### Visual Description
Icon/Small Image (29x29)
</details>
Resolver.
To conduct effective step-wise reasoning during proof by contradiction, we adhere to the resolution principle Robinson (1965) as it provides clear and concise instructions to resolve logical conflicts, minimizing the likelihood of reasoning errors. Specifically, it works by canceling out the complementary terms identified by the Search Router and connecting the remaining terms, a process that will be implemented using an LLM. Specifically, given two clauses $C_{\text{current}}$ and $C_{\text{complement}}$ , where:
$$
C_{\text{current}}=P(x,\text{True})\lor A
$$
$$
C_{\text{complement}}=P(x,\text{False})\lor B
$$
Here, $P(x,\text{True})$ and $P(x,\text{False})$ are complementary terms. The Resolver cancels out them and connects the remaining terms. The resolved clause becomes:
$$
C_{\text{resolved}}=\text{Resolve}(C_{\text{current}},C_{\text{complement}})=A\lor B
$$
If the remaining clause is empty or contradiction ( $\bot$ ) E.g. Resolve $C_{\text{current}}=(A)$ and $C_{\text{complement}}=(\neg A)$ will get an empty clause $C_{\text{resolved}}=\bot$ . An empty clause is equivalent to a contradiction. , we can conclude the proof and determine the answer, which will be explained in detail in Section 3 at Step 2.
## 3 Logic-Complete Reasoning Processing
With Aristotle, we now demonstrate how each module comes into play to form the integrated dual-path reasoning process.
#### Step 1: Search Initialization.
As shown in the step 1 of Fig. 2, given the original premises $P$ and the question statement $S$ , we first translate them into symbolic format $P_{t}$ and $S_{t}$ , and then decompose them into $P_{n}$ and $S_{n}$ , respectively.
Translate and Decompose $\blacktriangleright$ Input: $P$ , $S$ $\blacktriangleright$ Output: $P_{n}$ , $S_{n}$ , $C_{\text{current}}$ = { $S_{n}$ , $\neg S_{n}$ }
To implement proof by contradiction, we initialize the current clause $C_{\text{current}}$ with both $S_{n}$ and its negation $\neg S_{n}$ , denoted as $C_{\text{current}}=S_{n}$ and $C_{\text{current}}=\neg S_{n}$ . Considering both $S_{n}$ and $\neg S_{n}$ is necessary because we need both proofs to scrupulously conclude an answer, which is marked in Eq. (1) and will be explained in detail later in Step 3.
#### Step 2: Search and Resolve.
At this stage, two reasoning paths are initiated: one from $C_{\text{current}}=S_{n}$ and the other from $C_{\text{current}}=\neg S_{n}$ , initialized in Step 1. We aim to reach a final answer using proof by contradiction for both paths, iteratively search for complementary clauses and resolve conflicts. This helps us systematically reach an accurate final answer more quickly. Specifically for each reasoning path, presented in the Step 2 of Fig. 2, the Search Router selects clauses $C_{\text{complement}}\in P_{n}$ that are complementary to $C_{\text{current}}$ .
Search $\blacktriangleright$ Input: $P_{n}$ , $C_{\text{current}}$ $\blacktriangleright$ Output: $C_{\text{complement}}$
The Resolver module then applies the resolution rule Resolve( $C_{\text{current}}$ , $C_{\text{complement}}$ ) to produce a new clause $C_{\text{resolved}}$ .
Resolve $\blacktriangleright$ Input: $C_{\text{current}}$ , $C_{\text{complement}}$ $\blacktriangleright$ Output: $C_{\text{resolved}}$
If the $C_{\text{resolved}}$ indicates a contradiction or confirms the absence of a contradiction, we then terminate the reasoning process. If not, we then update $C_{\text{current}}$ = $C_{\text{resolved}}$ and repeat the Search and Resolve process. If the process reaches the maximum number of iterations $I_{\text{max}}$ and still does not find a contradiction, we conclude that there is no contradiction and terminate the reasoning process. Given the determination of whether contradiction exists, we then use the formula presented below to formally establish the proof $D_{S_{n}}$ (started from $C_{\text{current}}$ = $S_{n}$ ) and $D_{\neg S_{n}}$ (started from $C_{\text{current}}$ = $\neg S_{n}$ ) to determine whether $P_{n}$ entails either $S_{n}$ or $\neg S_{n}$ .
Proof Determination $D_{S_{n}}=\begin{cases}P_{n}\vdash\neg S_{n}&\text{($C_{\text{resolved}}$ = Contradiction)}\\ P_{n}\not\vdash\neg S_{n}&\text{($C_{\text{resolved}}$ = No Contradiction)}\end{cases}$ $D_{\neg S_{n}}=\begin{cases}P_{n}\vdash S_{n}&\text{($C_{\text{resolved}}$ = Contradiction)}\\ P_{n}\not\vdash S_{n}&\text{($C_{\text{resolved}}$ = No Contradiction)}\end{cases}$
#### Step 3: Conclude Answer.
This proof $D_{S_{n}}$ and $D_{\neg S_{n}}$ can then be used to conclude the truth value $A$ of $S$ based on Eq. (1). For example, consider a statement $S$ . If we get $D_{S_{n}}$ = $P\vdash\neg S$ and $D_{\neg S_{n}}$ = $P\not\vdash S$ , the combination of $P\vdash\neg S$ and $P\not\vdash S$ leads to the conclusion $A$ that $S$ is false according to Eq. (1).
Final Answer $\blacktriangleright$ Input: $D_{S_{n}}\in\left\{P_{n}\vdash\neg S_{n},P_{n}\not\vdash\neg S_{n}\right\}$ $D_{\neg S_{n}}\in\left\{P_{n}\vdash S_{n},P_{n}\not\vdash S_{n}\right\}$ $\blacktriangleright$ Output: $A\in\{\text{True, False, Unknown, Self-Contradictory}\}$
$$
A=\left\{\begin{array}[]{ll}\text{True,}&P_{n}\vdash S_{n}\land P_{n}\not\vdash\neg S_{n}\\
\text{False,}&P_{n}\not\vdash S_{n}\land P_{n}\vdash\neg S_{n}\\
\text{Unknown,}&P_{n}\not\vdash S_{n}\land P_{n}\not\vdash\neg S_{n}\\
\text{Self-Contradictory,}&P_{n}\vdash S_{n}\land P_{n}\vdash\neg S_{n}\\
\end{array}\right. \tag{1}
$$
The full algorithm and an example case can be found in Appendix H and I, respectively.
| | Method | GPT-4 | GPT-4o | | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| ProntoQA | ProofWriter | LogicNLI | Avg | ProntoQA | ProofWriter | LogicNLI | Avg | | |
| LR | Naive | 77.4 | 53.1 | 49.0 | 59.8 | 89.6 | 48.7 | 53.0 | 63.8 |
| CoT | 98.9 | 68.1 | 51.0 | 72.6 | 98.0 | 77.2 | 61.0 | 78.7 | |
| AR | CoT-SC | 93.4 | 69.3 | 57.3 | 73.3 | 99.6 | 78.3 | 64.3 | 80.7 |
| CR | 98.2 | 71.7 | 62.0 | 77.3 | 99.6 | 82.2 | 61.0 | 80.9 | |
| DetermLR | 98.6 | 79.2 | 57.0 | 78.3 | 93.4 | 69.8 | 58.0 | 75.7 | |
| ToT | 97.6 | 70.3 | 52.7 | 73.5 | 98.6 | 69.0 | 56.7 | 74.8 | |
| SR | SymbCoT | 99.6 | 82.5 | 59.0 | 80.4 | 99.4 | 82.3 | 58.7 | 80.1 |
| Logic-LM | 83.2 | 79.7 | - | - | 83.2 | 72.0 | - | - | |
| Ours | 99.6 | 86.8 | 68.3 | 84.9 | 99.6 | 88.5 | 70.7 | 86.3 | |
| (+0.0) | (+4.3) | (+6.3) | (+4.5) | (+0.0) | (+6.2) | (+6.4) | (+5.4) | | |
Table 1: Performance on GPT-4 and GPT-4o. The second best score is underlined and bold one is the best. In the brackets are the corresponding improvements in between.
## 4 Experiments
We present the experiment settings, baselines and results in this Section.
| $\bullet$ Claude-3.5-Sonnet CoT-SC | ProntoQA 98.0 | ProofWriter 78.5 | LogicNLI 54.3 | Avg 77.0 |
| --- | --- | --- | --- | --- |
| CR | 88.8 | 57.8 | 57.7 | 68.1 |
| ToT | 92.0 | 69.5 | 46.7 | 69.4 |
| Ours | 99.0 | 86.5 | 61.3 | 82.3 |
| (+1.0) | (+8.0) | (+3.6) | (+5.3) | |
| $\bullet$ Llama-3.1-405b | | | | |
| CoT-SC | 84.0 | 69.5 | 60.3 | 71.3 |
| CR | 96.0 | 56.3 | 50.7 | 67.7 |
| ToT | 98.4 | 65.5 | 56.7 | 73.5 |
| Ours | 98.4 | 89.5 | 69.0 | 85.6 |
| (+0.0) | (+20.0) | (+8.7) | (+12.1) | |
Table 2: Performance by using Claude-3.5-Sonnet and Llama-3.1-405B LLMs.
### 4.1 Settings
#### LLMs.
We assess the baselines and our method using GPT-4 and GPT-4o. We also include Claude and LLaMA to verify whether our method can generalize to different LLMs other than GPT series.
#### Dataset.
We evaluated both the baselines and our method on three carefully selected logical reasoning datasets: ProntoQA Saparov and He (2023), ProofWriter Tafjord et al. (2021) and LogicNLI Tian et al. (2021). These datasets were chosen to reflect increasing levels of difficulty, with ProntoQA being the easiest, ProofWriter moderately complex, and LogicNLI the most challenging due to their intricate logical structures. ProntoQA focuses on basic deductive logical relationships, ProofWriter introduces more complex structures such as “and/or,” and LogicNLI presents the most intricate reasoning with constructs such as “either/or” and “if and only if”. This progression enables us to comprehensively evaluate the effectiveness of our method across varying levels of complexity in logical structure. The details of each dataset can be found in appendix D.
#### Baselines.
We compare with a wide range of established baselines. Those baselines can be classified into three main categories. (1) Linear Reasoning (LR) refers to approaches where the model arrives at an answer through a single-step process, using a straightforward response based on the initial prompt including: Naive Prompting and CoT Wei et al. (2022); (2) Aggregative Reasoning (AR) refers to methods where the model performs reasoning multiple times or aggregates the results to reach a final answer. This includes: CoT-SC Wang et al. (2023b); Cumulative Reasoning (CR; Zhang et al., 2023); DetermLR Sun et al. (2024); ToT Yao et al. (2023); (3) Symbolic Reasoning (SR), which engages symbolic expressions and rules in the reasoning framework including: SymbCoT Xu et al. (2024) and Logic-LM Pan et al. (2023). More details can be found in Appendix G.
### 4.2 Main Result
The main results are presented in Table 1, from which we can learn the following observations:
#### Our method consistently outperforms all baselines across the three datasets.
Specifically, we achieve average improvements over CoT-SC, ToT, CR, and SymbCoT of 11.6%, 11.4%, 7.6%, and 4.5% on GPT-4, and 5.6%, 11.5%, 5.4%, and 6.2% on GPT-4o, respectively. These results demonstrate the general advantage of our method over the existing baselines across different datasets.
#### Our method performs even more effectively in complex logical scenarios.
We notice in Table 1 that our approach does not yield an improvement on the ProntoQA dataset. This can be attributed to the relative simplicity of the dataset, where most baselines already achieve high accuracy, leaving limited room for further enhancement. However, our improvements are more pronounced on the challenging datasets. Specifically, we achieve a 4.3% and 6.2% improvement over the second-best baseline on ProofWriter with GPT-4 and GPT-4o, respectively. On the most challenging dataset, LogicNLI, we observe even greater improvements of 6.3% for GPT-4 and 6.4% for GPT-4o. These results highlight the advantages of our method in scenarios involving complex logical structures and increased difficulty.
#### Our method is generalizable across different models.
In Table 2, we present the results for two models (Claude and Llama) outside the GPT series. We compare our method with strong baselines that aggregate multiple reasoning paths. Our method demonstrates similar improvements over the selected strong baseline, highlighting its generalizability across different models.
<details>
<summary>x9.png Details</summary>
### Visual Description
\n
## Bar Chart: Accuracy Comparison of Models
### Overview
This bar chart compares the accuracy of different model configurations on two datasets: ProofWriter and LogicNLI. The chart displays accuracy percentages for a baseline model ("Ours") and variations where specific components are removed ("w/o Decomposer", "w/o Search Router", "w/o Resolver").
### Components/Axes
* **X-axis:** Represents the datasets: "ProofWriter" and "LogicNLI".
* **Y-axis:** Represents "Accuracy (%)", ranging from approximately 30% to 90%.
* **Legend:**
* Dark Red: "Ours" (Baseline model)
* Medium Red: "w/o Decomposer" (Model without the Decomposer component)
* Light Red: "w/o Search Router" (Model without the Search Router component)
* Pale Red: "w/o Resolver" (Model without the Resolver component)
### Detailed Analysis
The chart consists of two sets of four bars, one for each dataset.
**ProofWriter Dataset:**
* "Ours" (Dark Red): The bar reaches approximately 88.5%.
* "w/o Decomposer" (Medium Red): The bar reaches approximately 62.0%.
* "w/o Search Router" (Light Red): The bar reaches approximately 47.1%.
* "w/o Resolver" (Pale Red): The bar reaches approximately 37.7%.
**LogicNLI Dataset:**
* "Ours" (Dark Red): The bar reaches approximately 70.7%.
* "w/o Decomposer" (Medium Red): The bar reaches approximately 42.8%.
* "w/o Search Router" (Light Red): The bar reaches approximately 39.1%.
* "w/o Resolver" (Pale Red): The bar reaches approximately 57.5%.
### Key Observations
* The "Ours" model consistently outperforms all variations across both datasets.
* Removing the "Decomposer" component results in a significant accuracy drop for both datasets, but the drop is more pronounced in ProofWriter.
* Removing the "Search Router" and "Resolver" components leads to substantial accuracy reductions, particularly in ProofWriter.
* The "w/o Resolver" model performs relatively better on LogicNLI compared to ProofWriter, while the other variations show a more consistent performance drop across datasets.
### Interpretation
The data suggests that all three components – Decomposer, Search Router, and Resolver – contribute significantly to the overall accuracy of the model. The Decomposer appears to be the most critical component, as its removal leads to the largest performance decrease. The difference in performance between the datasets suggests that the importance of each component may vary depending on the characteristics of the data. The ProofWriter dataset seems to be more sensitive to the removal of the Search Router and Resolver components than the LogicNLI dataset. This could indicate that ProofWriter requires more sophisticated search and resolution mechanisms. The chart demonstrates the importance of each component in the model architecture and provides insights into their relative contributions to performance. The consistent outperformance of the "Ours" model highlights the effectiveness of the complete architecture.
</details>
Figure 3: Ablation results (w/ GPT-4o).
### 4.3 Model Ablation
To evaluate the contribution of each module in our framework, we conducted an ablation study by replacing each module individually with simpler alternatives. Specifically, we substitute (1) the Decomposer by prompting the LLM for simple decomposition, (2) the Resolver by prompting the LLM to infer using the given premises, and (3) the Search Router by prompting the LLM to search for relevant premises.
The results, shown in Fig. 3, demonstrate that removing any module leads to a significant performance drop, highlighting the importance of each component. Notably, replacing the Search Router results in the largest performance decline (50.8% and 31.6% for ProofWriter and LogicNLI, respectively), emphasizing the benefits of searching complementary premises under the proof-by-contradiction strategy. Besides, the Decomposer has a greater impact than the Resolver on LogicNLI, whereas in ProofWriter, the Resolver plays a more significant role than the Decomposer. This is because LogicNLI includes more complex logical structures, such as “either…or…”, “vice versa”, and “if and only if”, while ProofWriter primarily involves simpler conjunctions such as “and”, “or”. As a result, LogicNLI relies more heavily on the Decomposer to break down complex logical statements into simpler forms for optimal performance.
## 5 Analysis and Discussion
We now take one step further, delving into the underlying working mechanisms of our system.
<details>
<summary>x10.png Details</summary>
### Visual Description
\n
## Scatter Plot: Accuracy vs. Number of Steps
### Overview
This image presents a scatter plot comparing the accuracy of different methods against the number of steps taken. The plot displays data points for "Ours", "DetermLR", "CR", "CoT-SC", and "ToT". The x-axis represents the number of steps, and the y-axis represents the accuracy in percentage.
### Components/Axes
* **X-axis:** Number of Steps (ranging from approximately 12 to 24).
* **Y-axis:** Accuracy (%) (ranging from approximately 65% to 95%).
* **Data Series/Labels:**
* "Ours" (represented by a red star)
* "DetermLR" (represented by blue circles)
* "CR" (represented by blue circles)
* "CoT-SC" (represented by blue circles)
* "ToT" (represented by blue circles)
* **Legend:** Located in the top-left corner, indicating the color and label for "Ours".
### Detailed Analysis
* **"Ours"**: A single data point at approximately (12, 86%).
* **"DetermLR"**: A data point at approximately (16, 79%).
* **"CR"**: A data point at approximately (16, 71%).
* **"CoT-SC"**: A data point at approximately (16, 69%).
* **"ToT"**: A data point at approximately (24, 70%).
### Key Observations
* "Ours" achieves the highest accuracy at 12 steps.
* The accuracy of "DetermLR", "CR", "CoT-SC", and "ToT" are all lower than "Ours".
* "CoT-SC" has the lowest accuracy among the methods evaluated.
* "ToT" requires 24 steps to achieve an accuracy of approximately 70%.
* The methods "DetermLR", "CR", "CoT-SC" all have the same number of steps (16).
### Interpretation
The data suggests that the "Ours" method outperforms the other methods ("DetermLR", "CR", "CoT-SC", and "ToT") in terms of accuracy, achieving a significantly higher accuracy with fewer steps. The other methods require more steps to achieve lower accuracy. This could indicate that "Ours" is a more efficient or effective method for the task being evaluated. The fact that "CoT-SC" consistently has the lowest accuracy suggests it may be less suitable for this task. The relatively low accuracy of "ToT" even at 24 steps suggests it may not be a scalable or efficient solution. The plot demonstrates a trade-off between the number of steps and accuracy, with "Ours" offering the best balance.
</details>
Figure 4: Accuracy vs. Efficiency on ProofWriter using GPT-4. Efficiency is measured as the average number of visited nodes/steps required to solve the problem. The upper-left corner is the optimal point, representing the best performance with the fewest visited nodes.
### 5.1 Accuracy vs. Efficiency
#### Our method achieves better reasoning accuracy with higher efficiency.
Here, we measure the average number of steps or nodes for solving problems in the ProofWriter dataset. As shown in Fig. 4, our method not only achieves the highest accuracy across all baselines but does so with the least number of visited nodes indicating both superior efficacy and efficiency. Specifically, our method achieves the highest accuracy among all baselines, while visiting only 11.65 nodes on average, reducing the number of nodes visited by 52.6%, 30.5%, and 20.4% compared to ToT, CR, and DetermLR, respectively. This demonstrates that our approach effectively balances accuracy and computational efficiency. By directly targeting contradictions, it significantly streamlines the reasoning process, making it both precise and efficient.
### 5.2 Step-wise Reasoning Accuracy
#### The
<details>
<summary>x11.png Details</summary>
### Visual Description
Icon/Small Image (29x29)
</details>
Resolver can achieve near-perfect accuracy in one-step logical inference.
To understand why our framework is effective, we must also examine its one-step logical reasoning accuracy. Since the final answer is derived from these individual inferences (i.e., nodes in ToT and steps in Ours), their accuracy directly impacts the overall performance. We compare the one-step reasoning accuracy of our method with that of ToT shown in Fig. 5. We randomly sample 100 cases with manual evaluation. ToT demonstrated around 70% accuracy, which is consistent with prior research showing that LLMs can sometimes introduce logical errors. In contrast, our Aristotle achieved near-perfect accuracy in one-step inference, underscoring the effectiveness of the Resolver module’s use of the resolution principle. This is because the resolution principle provides a systematic and logically rigorous way to resolve contradictions, simplifying the reasoning process compared to methods that rely on LLMs to reason from previous steps and multiple premises.
<details>
<summary>x12.png Details</summary>
### Visual Description
\n
## Bar Chart: One-step Inference Accuracy
### Overview
This bar chart compares the one-step inference accuracy of two models, "ToT" and "Ours", across two datasets: "ProofWriter" and "LogicNLI". The chart displays accuracy percentages, with a clear visual emphasis on the improvement achieved by the "Ours" model compared to "ToT".
### Components/Axes
* **Title:** "One-step Inference Accuracy" (centered at the top)
* **X-axis:** Datasets - "ProofWriter" and "LogicNLI" (horizontally aligned at the bottom)
* **Y-axis:** Accuracy (%) - ranging from 60% to 100% (vertically aligned on the left)
* **Legend:** Located at the bottom-center of the chart.
* "ToT" - represented by a blue color.
* "Ours" - represented by a red color.
* **Improvement Arrows:** Red arrows indicating the percentage point increase in accuracy from "ToT" to "Ours" for each dataset.
* **Dashed Lines:** Horizontal dashed lines at approximately 70% accuracy, visually connecting the "ToT" bars.
### Detailed Analysis
The chart consists of four bars, two for each dataset.
**ProofWriter Dataset:**
* **ToT (Blue Bar):** The blue bar for ProofWriter starts at approximately 74.0%. The bar extends to approximately 74.0% on the Y-axis.
* **Ours (Red Bar):** The red bar for ProofWriter starts at approximately 74.0% (aligned with the ToT bar) and extends to approximately 99.7% on the Y-axis.
* **Improvement Arrow:** A red arrow points upwards from the ToT bar to the Ours bar, indicating an improvement of 25.7%.
**LogicNLI Dataset:**
* **ToT (Blue Bar):** The blue bar for LogicNLI starts at approximately 69.2%. The bar extends to approximately 69.2% on the Y-axis.
* **Ours (Red Bar):** The red bar for LogicNLI starts at approximately 69.2% (aligned with the ToT bar) and extends to approximately 99.5% on the Y-axis.
* **Improvement Arrow:** A red arrow points upwards from the ToT bar to the Ours bar, indicating an improvement of 30.3%.
### Key Observations
* The "Ours" model consistently outperforms the "ToT" model on both datasets.
* The improvement in accuracy is more significant on the LogicNLI dataset (30.3%) compared to the ProofWriter dataset (25.7%).
* Both models achieve relatively low accuracy with "ToT" on both datasets, but "Ours" achieves very high accuracy (close to 100%) on both datasets.
### Interpretation
The data strongly suggests that the "Ours" model represents a substantial improvement over the "ToT" model in one-step inference accuracy for both ProofWriter and LogicNLI datasets. The consistent and significant gains in accuracy indicate that the "Ours" model has learned more effective representations or inference strategies for these tasks. The larger improvement on LogicNLI might suggest that the "Ours" model is particularly well-suited for the types of logical reasoning challenges present in that dataset. The near-perfect accuracy achieved by "Ours" on both datasets is a notable result, suggesting a high level of performance. The dashed lines at 70% accuracy serve to highlight the dramatic increase in performance achieved by the "Ours" model.
</details>
Figure 5: One-step reasoning accuracy using GPT-4o.
### 5.3 Search Error
#### Our method effectively reduces errors from the search strategy.
Apart from one-step logical inference, the search router also plays a crucial role. Previous research has shown that methods involving an evaluator to guide the search tend to underperform as the evaluator can be unreliable and may mislead the reasoning process, resulting in incorrect answers. We assess the search error In ToT, search errors occur when the evaluator selects a logically flawed node for expansion. In contrast, in our method, search errors arise when either the complementary clause is not found or a non-complementary clause is selected. The evaluation process is conducted manually., as shown in Fig. 6. Our search strategy significantly reduces errors, lowering them by 11.2% in ProofWriter and 9.0% in LogicNLI. This demonstrates that our logic-based search approach outperforms LLM self-evaluation, effectively addressing the limitations posed by unreliable evaluators in logical reasoning. An explanation is that our method simplifies the search process by focusing on identifying complementary clauses, a task with clear definitions and rules that an LLM can easily follow with a few examples. In contrast, having an LLM evaluate logical inferences, such as in ToT, requires complex judgments, making it more prone to errors Chen et al. (2024); Wang et al. (2024b).
<details>
<summary>x13.png Details</summary>
### Visual Description
\n
## Bar Chart: Search Error
### Overview
This bar chart compares the error rates of different search methods (ToT, Ours, ToT-Search, Ours-Search) across two datasets (ProofWriter and LogicNLI). The error rate is measured in percentage (%). The chart uses stacked bars to represent the contribution of each method to the overall error rate.
### Components/Axes
* **Title:** "Search Error" (centered at the top)
* **X-axis:** Datasets - "ProofWriter" and "LogicNLI" (horizontally aligned at the bottom)
* **Y-axis:** Error Rate (%) - ranging from 0% to 45% (vertically aligned on the left)
* **Legend:** Located at the bottom-right corner.
* "ToT" - Light Blue
* "ToT-Search" - Dark Blue
* "Ours" - Light Red
* "Ours-Search" - Dark Red
### Detailed Analysis
The chart consists of two sets of stacked bars, one for each dataset.
**ProofWriter Dataset:**
* **ToT (Light Blue):** Approximately 31.0%
* **ToT-Search (Dark Blue):** Approximately 14.0%
* **Ours (Light Red):** Approximately 11.5%
* **Ours-Search (Dark Red):** Approximately 2.8%
* Total Error Rate: 31.0% + 14.0% + 11.5% + 2.8% = 59.3% (This is not a direct reading from the chart, but the sum of the stacked components)
**LogicNLI Dataset:**
* **ToT (Light Blue):** Approximately 43.2%
* **ToT-Search (Dark Blue):** Approximately 16.0%
* **Ours (Light Red):** Approximately 29.5%
* **Ours-Search (Dark Red):** Approximately 5.0%
* Total Error Rate: 43.2% + 16.0% + 29.5% + 5.0% = 93.7% (This is not a direct reading from the chart, but the sum of the stacked components)
The bars are stacked, meaning the height of each segment represents the error rate contributed by that specific method.
### Key Observations
* "Ours-Search" consistently exhibits the lowest error rate across both datasets.
* "ToT" has the highest error rate in the LogicNLI dataset.
* The total error rate is significantly higher for the LogicNLI dataset compared to the ProofWriter dataset.
* The "Ours" method has a higher error rate than "ToT-Search" in the ProofWriter dataset, but a lower error rate in the LogicNLI dataset.
### Interpretation
The chart demonstrates the effectiveness of the "Ours-Search" method in reducing search errors compared to other methods ("ToT", "ToT-Search", and "Ours") across both datasets. The LogicNLI dataset presents a higher overall error rate, suggesting it is a more challenging dataset for all search methods. The performance difference between "Ours" and "ToT-Search" varies depending on the dataset, indicating that the optimal method may depend on the specific characteristics of the data. The stacked bar format effectively visualizes the contribution of each method to the overall error rate, allowing for a clear comparison of their performance. The data suggests that the "Ours-Search" method is a significant improvement over the other methods, particularly in reducing the overall error rate.
</details>
Figure 6: The outer bar shows the overall error rate. The inner bar represents the proportion of the error caused by the search strategy.
### 5.4 Complex Reasoning
#### Our method demonstrates a clear advantage in handling problems of increasing difficulty.
We evaluate accuracy across different reasoning difficulties in ProofWriter, as shown in Fig. 7. Our method consistently outperforms others at all depths, maintaining superior accuracy. It excels particularly at moderate and challenging depths, surpassing baselines like SymbCoT and Logic-LM. Even as other methods struggle at higher depths, our approach remains robust, demonstrating better scalability and resilience to problem difficulty. This effectiveness is due to two main factors: (1) using the resolution principle minimizes errors at each step and prevents them from compounding, and (2) streamlining the reasoning process reduces steps, lowering the likelihood of error accumulation.
<details>
<summary>x14.png Details</summary>
### Visual Description
\n
## Line Chart: Accuracy vs. Reasoning Depth
### Overview
This line chart depicts the relationship between Reasoning Depth and Accuracy (%) for four different models: CoT, Logic-LM, SymbCoT, and "Ours". The chart shows how the accuracy of each model changes as the reasoning depth increases from 0 to 5.
### Components/Axes
* **X-axis:** Reasoning Depth (ranging from 0 to 5).
* **Y-axis:** Accuracy (%) (ranging from 50% to 100%).
* **Legend:** Located in the bottom-center of the chart, identifying the four data series:
* CoT (Blue, Triangle Marker)
* Logic-LM (Dark Blue, Circle Marker)
* SymbCoT (Light Blue, Star Marker)
* Ours (Red, Diamond Marker)
* **Gridlines:** Horizontal and vertical gridlines are present to aid in reading values.
### Detailed Analysis
Here's a breakdown of each data series, with approximate values:
* **CoT (Blue, Triangle):** The line slopes downward consistently.
* Reasoning Depth 0: ~82%
* Reasoning Depth 1: ~78%
* Reasoning Depth 2: ~72%
* Reasoning Depth 3: ~68%
* Reasoning Depth 5: ~51%
* **Logic-LM (Dark Blue, Circle):** The line also slopes downward, but less steeply than CoT.
* Reasoning Depth 0: ~78%
* Reasoning Depth 1: ~75%
* Reasoning Depth 2: ~69%
* Reasoning Depth 3: ~65%
* Reasoning Depth 5: ~68%
* **SymbCoT (Light Blue, Star):** This line starts high and decreases, then flattens out.
* Reasoning Depth 0: ~92%
* Reasoning Depth 1: ~89%
* Reasoning Depth 2: ~65%
* Reasoning Depth 3: ~82%
* Reasoning Depth 5: ~75%
* **Ours (Red, Diamond):** This line starts at the highest accuracy and decreases, but remains relatively high throughout.
* Reasoning Depth 0: ~98%
* Reasoning Depth 1: ~94%
* Reasoning Depth 2: ~90%
* Reasoning Depth 3: ~85%
* Reasoning Depth 5: ~78%
### Key Observations
* "Ours" consistently outperforms the other models across all reasoning depths.
* CoT exhibits the most significant decrease in accuracy as reasoning depth increases.
* SymbCoT shows a notable drop in accuracy between reasoning depths 1 and 2.
* Logic-LM maintains a relatively stable accuracy compared to the other models.
### Interpretation
The data suggests that the "Ours" model is more robust to increased reasoning depth than the other models (CoT, Logic-LM, and SymbCoT). As the reasoning depth increases, the accuracy of CoT, Logic-LM, and SymbCoT declines, indicating a potential limitation in their ability to maintain performance with more complex reasoning chains. The initial high performance of SymbCoT is interesting, but its subsequent drop suggests it may be sensitive to specific types of reasoning challenges. The relatively stable performance of Logic-LM could indicate a different approach to reasoning that is less susceptible to depth-related issues. The consistent high accuracy of "Ours" suggests a more effective reasoning mechanism or a better ability to handle the complexities introduced by increased reasoning depth. The chart highlights the importance of considering reasoning depth when evaluating the performance of language models and suggests that "Ours" is a promising approach for tasks requiring deeper reasoning capabilities.
</details>
Figure 7: Studying the effect of reasoning depth with GPT-4 on ProofWriter.
#### The cost scaling is stable with increased reasoning depth.
To complement the performance analysis on different reasoning depth, we also address concerns about the scalability of our framework when applied to tasks requiring deeper reasoning involving greater reasoning depth. Specifically, we provide a detailed examination of the marginal computational costs and token usage associated with extended reasoning chains. Aristotle is designed to handle increased reasoning depth in an efficient and controlled manner.
Each reasoning step in our framework consists of two operations. First, a search operation is performed using a deterministic rule-based method, which introduces minimal computational overhead and does not contribute additional token usage as reasoning depth increases. Second, a resolve operation is executed by the resolver module, which processes one reasoning step at a time and is the only component contributing to token-based computational cost.
This modular design ensures that total token usage grows linearly with the number of reasoning steps, keeping the marginal cost per additional step low and predictable. To empirically validate the efficiency and stability of our approach, we analyzed token usage for individual reasoning steps across two benchmark datasets, ProofWriter and LogicNLI, as shown in Table 3. The statistics indicate that token usage per reasoning step is highly consistent, exhibiting low standard deviation and coefficient of variation. Moreover, the absolute token cost per step remains modest, ensuring that deeper reasoning does not impose a significant computational burden. Given the stable, linear scaling of token consumption and the low per-step cost, our framework maintains its efficiency even for tasks requiring extended reasoning chains.
| ProofWriter LogicNLI | 3076.8 2071.1 | 19.1 26.4 | 0.71% 0.85% |
| --- | --- | --- | --- |
Table 3: Token usage statistics per reasoning step. TU denotes Token Usage, Std. Dev. denotes Standard Deviation, and CV denotes Coefficient of Variation.
<details>
<summary>x15.png Details</summary>
### Visual Description
\n
## Pie Charts: Error Distribution for ProofWriter and LogicNLI
### Overview
The image presents two pie charts, side-by-side, illustrating the distribution of different error types for two systems: ProofWriter and LogicNLI. Each slice of the pie charts represents the percentage of errors falling into a specific category. The legend at the bottom identifies the error categories and their corresponding colors.
### Components/Axes
The charts are pie charts, with each slice representing a percentage of the total errors. There are no explicit axes, as pie charts represent proportions of a whole. The legend, positioned at the bottom of the image, provides the following mapping:
* **Translation:** (Salmon/Peach color)
* **Resolve:** (Light Pink color)
* **Imax:** (Light Blue color)
* **Decompose:** (Light Green color)
* **Search:** (Pale Yellow color)
* **Contra Error:** (Dark Gray color)
The titles of the charts are "ProofWriter" (left) and "LogicNLI" (right), positioned above each respective pie chart. Each slice is labeled with a percentage value.
### Detailed Analysis or Content Details
**ProofWriter (Left Chart):**
* **Contra Error:** 27.0% (Dark Gray slice, positioned at the top)
* **Translation:** 24.3% (Salmon/Peach slice, positioned to the left of Contra Error)
* **Imax:** 18.9% (Light Blue slice, positioned below Translation)
* **Decompose:** 10.8% (Light Green slice, positioned below Imax)
* **Search:** 10.8% (Pale Yellow slice, positioned to the right of Decompose)
* **Resolve:** 8.1% (Light Pink slice, positioned to the right of Search)
**LogicNLI (Right Chart):**
* **Contra Error:** 33.3% (Dark Gray slice, positioned at the top)
* **Translation:** 23.8% (Salmon/Peach slice, positioned to the left of Contra Error)
* **Resolve:** 16.7% (Light Pink slice, positioned below Translation)
* **Search:** 9.5% (Pale Yellow slice, positioned below Resolve)
* **Imax:** 9.5% (Light Blue slice, positioned to the right of Search)
* **Decompose:** 7.1% (Light Green slice, positioned to the right of Imax)
### Key Observations
* **Contra Error** is the most significant error type for both ProofWriter and LogicNLI, accounting for 27.0% and 33.3% of errors respectively.
* **Translation** errors are also substantial in both systems, at 24.3% for ProofWriter and 23.8% for LogicNLI.
* **Resolve** errors are relatively low in ProofWriter (8.1%) but higher in LogicNLI (16.7%).
* **Decompose** errors are more prominent in ProofWriter (10.8%) than in LogicNLI (7.1%).
* **Search** errors are similar in both systems, around 10%.
* **Imax** errors are similar in both systems, around 10%.
### Interpretation
The data suggests that both ProofWriter and LogicNLI struggle most with "Contra Error" and "Translation" issues. The higher percentage of "Contra Error" in LogicNLI might indicate a more fundamental difficulty in handling contradictory information or logical inconsistencies within that system. The relatively higher proportion of "Resolve" errors in LogicNLI could suggest challenges in resolving ambiguities or completing inferences. The differences in "Decompose" errors might point to variations in how each system breaks down complex problems into simpler steps.
The consistent prominence of "Contra Error" and "Translation" across both systems suggests these are common challenges in the domain of natural language inference and reasoning. Further investigation into the specific instances of these errors could reveal underlying patterns and inform improvements to both ProofWriter and LogicNLI. The pie charts provide a clear visual comparison of the error profiles of the two systems, highlighting their strengths and weaknesses.
</details>
Figure 8: Error analysis on ProofWriter and LogicNLI with GPT-4o.
### 5.5 Error Analysis
To thoroughly understand the limitations of our framework, we conduct a manual error analysis on the ProofWriter and LogicNLI datasets using GPT-4o. The detailed error statistics are presented in Fig. F.
The majority of errors stem from the Contradiction Error, primarily due to flaws in dataset construction. The next most common source is the Search module, where complementary clauses exist but are not retrieved. This is often due to unexpected symbols (e.g., LaTeX code) in the LLM’s output that disrupt regular expression matching.
Translation and Decomposition errors are the third largest category. These occur when the LLM struggles to parse complex logical relationships or convert them into the correct symbolic form. Such errors are more prevalent in LogicNLI, which features more intricate constructs (e.g., "either…or…" and "if and only if") compared to the simpler logic in ProofWriter (e.g., "and," "or").
Another notable source of error is Insufficient Iterations, where the reasoning process terminates prematurely, often concluding "No contradiction" when further iterations might reveal one. While increasing the iteration threshold could mitigate this, it must be balanced against computational efficiency.
Finally, Resolution errors, often due to incorrect variable instantiations, are relatively infrequent. This is because logical statements have been reduced to a simple conjunctive normal form (CNF) by this point, making them easier to interpret, and the resolution principle offers clear guidance for resolving inconsistencies.
Potential improvements include incorporating more targeted in-context learning (ICL) examples to enhance translation and resolution. Besides, enhancing regular expression patterns to accommodate a wider range of syntactic variations could further reduce search errors. Additionally, tuning iteration limits would help achieve a better balance between accuracy and computational efficiency. More details of error analysis can be found at Appendix F.
## 6 Related Work
Enhancing the logical reasoning of LLMs to achieve human-like levels has been a key focus in recent research Huang and Chang (2023); Dunivin (2024). Existing approaches can be broadly categorized into the following:
#### Linear Reasoning.
These approaches involve prompting LLMs once to emulate human reasoning in a sequential manner. The representative is the CoT method Wei et al. (2022), which guides the model to generate reasoning steps linearly. Building upon CoT, SymbCoT Xu et al. (2024) incorporates symbolic expressions and rules into the linear reasoning process to achieve more rigorous logical reasoning. However, these methods lack any searching or backtracking mechanism to avoid flawed reasoning paths, leading to suboptimal performance. In this paper, we thus consider the searching-based reasoning framework.
#### Sampling Methods.
These methods obtain the final answer through samplings to enhance reasoning diversity and accuracy Wang et al. (2023b); Fu et al. (2023); Manakul et al. (2023). This involves running the reasoning process multiple times, with the increased diversity of reasoning paths contributing to better results. However, they do not resolve the underlying issue of flawed logical reasoning inherent to the LLM, which is resolved by the resolution principle Robinson (1965) in our framework.
#### Iterative Reasoning with Search.
These methods rely on an evaluator to search for different reasoning paths to avoid flawed nodes. Techniques such as ToT Yao et al. (2023), and its variances Xie et al. (2023); Zhang et al. (2023); Sun et al. (2024), generate multiple thoughts during the reasoning. An evaluator repetitively selects the most probable paths to expand to the next level until the final answer. However, the evaluator may not be reliable Chen et al. (2024); Wang et al. (2024b), potentially selecting incorrect nodes for expansion and propagating errors. This paper proposes a search mechanism that relies on matching symbolic logic, avoiding the use of an unreliable evaluator.
#### Reasoning Relying on External Tools.
Here LLMs often involve integrating well-developed rule-based reasoning engines, where LLMs act as mere translators, converting the natural language of reasoning questions into specific symbolic forms to be processed by external rule-based engines. Examples include Logic-LM Pan et al. (2023), LINC Olausson et al. (2023) and PAL Gao et al. (2023). The limitation of this approach lies in the strict formatting requirements of external logic resolver; LLMs inevitably introduce syntax errors during translation, leading to failures in the reasoning process. Fortunately, the success of SymbCoT Xu et al. (2024) preliminarily demonstrates that enabling LLMs to perform logical reasoning based on symbols is feasible and promising. In our paper, we further prove that symbolic logic expressions can be fully integrated into all processes of the reasoning framework, including decomposition, search, and inference, thereby demonstrating that LLMs themselves can completely achieve high-level symbolic logical reasoning.
## 7 Conclusion
We presented Aristotle, a logic-complete reasoning framework designed to tackle the challenges of logical reasoning, which comprehensively integrates symbolic expressions and logical rules into three core components: Logical Decomposer, Logical Search Router, and Logical Resolver. These modules streamline the reasoning process by reducing the task complexity, minimizing the search errors, and rigorously resolving logical contradictions. Our experiments show that our method consistently outperforms state-of-the-art frameworks in both accuracy and efficiency significantly.
## Acknowledgements
This work is supported by the Ministry of Education, Singapore, under its MOE AcRF TIER 3 Grant (MOE-MOET32022-0001).
## Potential Limitations
Our method faces two potential limitations. First, the reasoning process relies on the quality of translation and decomposition. However, even with a few-shot approach, LLMs cannot always guarantee that these processes are fully correct. Future work could consider more advanced methods to guarantee the quality of these processes, such as fine-tuning. Secondly, our reasoning approach requires that all necessary information is explicitly stated in the premises. If any implicit information or assumptions exist, our method may fail to capture them, leading to incorrect reasoning. A more detailed analysis of this limitation is provided in Appendix E. Nevertheless, there are existing methods that explore how to make implicit information explicit. Future work could integrate those methods into this framework to address this limitation.
## Ethics Statement
The datasets employed in our research were carefully selected from publicly available or ethically sourced materials, and we take deliberate steps to identify and reduce biases within these datasets to uphold fairness in our outcomes.
## References
- Baader et al. (2003) Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press.
- Besta et al. (2024) Maciej Besta, Nils Blach, Ales Kubicek, Robert Gerstenberger, Michal Podstawski, Lukas Gianinazzi, Joanna Gajda, Tomasz Lehmann, Hubert Niewiadomski, Piotr Nyczyk, and Torsten Hoefler. 2024. Graph of thoughts: Solving elaborate problems with large language models. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 17682–17690, Vancouver, Canada.
- Bishop (1967) Errett Bishop. 1967. Foundations of Constructive Analysis. Mcgraw-Hill.
- Chen et al. (2024) Ziru Chen, Michael White, Ray Mooney, Ali Payani, Yu Su, and Huan Sun. 2024. When is tree search useful for LLM planning? It depends on the discriminator. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pages 13659–13678, Bangkok, Thailand.
- Chowdhery et al. (2023) Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emily Reif, Nan Du, Ben Hutchinson, Reiner Pope, James Bradbury, Jacob Austin, Michael Isard, Guy Gur-Ari, Pengcheng Yin, Toju Duke, Anselm Levskaya, Sanjay Ghemawat, Sunipa Dev, Henryk Michalewski, Xavier Garcia, Vedant Misra, Kevin Robinson, Liam Fedus, Denny Zhou, Daphne Ippolito, David Luan, Hyeontaek Lim, Barret Zoph, Alexander Spiridonov, Ryan Sepassi, David Dohan, Shivani Agrawal, Mark Omernick, Andrew M. Dai, Thanumalayan Sankaranarayana Pillai, Marie Pellat, Aitor Lewkowycz, Erica Moreira, Rewon Child, Oleksandr Polozov, Katherine Lee, Zongwei Zhou, Xuezhi Wang, Brennan Saeta, Mark Diaz, Orhan Firat, Michele Catasta, Jason Wei, Kathy Meier-Hellstern, Douglas Eck, Jeff Dean, Slav Petrov, and Noah Fiedel. 2023. Palm: Scaling language modeling with pathways. Journal of Machine Learning Research, 24:240:1–240:113.
- Clocksin and Mellish (2003) William F Clocksin and Christopher S Mellish. 2003. Programming in Prolog. Springer Science & Business Media.
- Cummins et al. (1991) D.D. Cummins, T. Lubart, O. Alksnis, et al. 1991. Conditional reasoning and causation. Memory & Cognition, 19:274–282.
- Davis and Putnam (1960) Martin Davis and Hilary Putnam. 1960. A computing procedure for quantification theory. J. ACM, 7(3):201–215.
- Dunivin (2024) Zackary Okun Dunivin. 2024. Scalable qualitative coding with LLMs: Chain-of-Thought reasoning matches human performance in some hermeneutic tasks. ArXiv preprint, abs/2401.15170.
- Eisner et al. (2024) Ben Eisner, Yi Yang, Todor Davchev, Mel Vecerík, Jonathan Scholz, and David Held. 2024. Deep se(3)-equivariant geometric reasoning for precise placement tasks. In The Twelfth International Conference on Learning Representations, Vienna, Austria.
- Fu et al. (2023) Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. 2023. Complexity-based prompting for multi-step reasoning. In The Eleventh International Conference on Learning Representations, Kigali, Rwanda.
- Gao et al. (2023) Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. 2023. PAL: program-aided language models. In International Conference on Machine Learning, volume 202, pages 10764–10799, Honolulu, Hawaii, USA. PMLR.
- Han et al. (2022) Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujie Qiao, Matthew Burtell, David Peng, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Shafiq R. Joty, Alexander R. Fabbri, Wojciech Kryscinski, Xi Victoria Lin, Caiming Xiong, and Dragomir Radev. 2022. FOLIO: natural language reasoning with first-order logic. ArXiv preprint, abs/2209.00840.
- Huang and Chang (2023) Jie Huang and Kevin Chen-Chuan Chang. 2023. Towards reasoning in large language models: A survey. In Findings of the Association for Computational Linguistics: ACL 2023, pages 1049–1065, Toronto, Canada.
- Li et al. (2024) Haoming Li, Zhaoliang Chen, Jonathan Zhang, and Fei Liu. 2024. LASP: surveying the state-of-the-art in large language model-assisted AI planning. ArXiv preprint, abs/2409.01806.
- Liu et al. (2023) Hanmeng Liu, Ruoxi Ning, Zhiyang Teng, Jian Liu, Qiji Zhou, and Yue Zhang. 2023. Evaluating the logical reasoning ability of ChatGPT and GPT-4. ArXiv preprint, abs/2304.03439.
- Liu et al. (2020) Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang. 2020. LogiQA: A challenge dataset for machine reading comprehension with logical reasoning. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, pages 3622–3628.
- Manakul et al. (2023) Potsawee Manakul, Adian Liusie, and Mark Gales. 2023. SelfCheckGPT: Zero-resource black-box hallucination detection for generative large language models. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 9004–9017, Singapore.
- Markovits and Vachon (1989) Henry Markovits and Robert Vachon. 1989. Reasoning with contrary-to-fact propositions. Journal of Experimental Child Psychology, 47:398–412.
- Ning et al. (2024) Xuefei Ning, Zinan Lin, Zixuan Zhou, Zifu Wang, Huazhong Yang, and Yu Wang. 2024. Skeleton-of-Thought: Prompting llms for efficient parallel generation. In The Twelfth International Conference on Learning Representations, Vienna, Austria.
- Nonnengart (1996) Andreas Nonnengart. 1996. Strong skolemization.
- Olausson et al. (2023) Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. LINC: A neurosymbolic approach for logical reasoning by combining language models with First-Order Logic provers. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 5153–5176, Singapore.
- Pan et al. (2023) Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, Singapore.
- Parmar et al. (2024) Mihir Parmar, Nisarg Patel, Neeraj Varshney, Mutsumi Nakamura, Man Luo, Santosh Mashetty, Arindam Mitra, and Chitta Baral. 2024. LogicBench: Towards systematic evaluation of logical reasoning ability of large language models. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pages 13679–13707, Bangkok, Thailand.
- Patel et al. (2023) Ajay Patel, Bryan Li, Mohammad Sadegh Rasooli, Noah Constant, Colin Raffel, and Chris Callison-Burch. 2023. Bidirectional language models are also few-shot learners. In The Eleventh International Conference on Learning Representations, Kigali, Rwanda.
- Patel et al. (2024) Nisarg Patel, Mohith Kulkarni, Mihir Parmar, Aashna Budhiraja, Mutsumi Nakamura, Neeraj Varshney, and Chitta Baral. 2024. Multi-LogiEval: Towards evaluating multi-step logical reasoning ability of large language models. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, pages 20856–20879, Bangkok, Thailand.
- Robinson (1965) John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23–41.
- Saparov and He (2023) Abulhair Saparov and He He. 2023. Language models are greedy reasoners: A systematic formal analysis of Chain-of-Thought. In The Eleventh International Conference on Learning Representations, Kigali, Rwanda.
- Sun et al. (2024) Hongda Sun, Weikai Xu, Wei Liu, Jian Luan, Bin Wang, Shuo Shang, Ji-Rong Wen, and Rui Yan. 2024. DetermLR: Augmenting LLM-based logical reasoning from indeterminacy to determinacy. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 9828–9862, Bangkok, Thailand.
- Tafjord et al. (2021) Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634.
- Tian et al. (2021) Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. 2021. Diagnosing the first-order logical reasoning ability through LogicNLI. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 3738–3747, Online and Punta Cana, Dominican Republic.
- Tyagi et al. (2024) Nemika Tyagi, Mihir Parmar, Mohith Kulkarni, Aswin RRV, Nisarg Patel, Mutsumi Nakamura, Arindam Mitra, and Chitta Baral. 2024. Step-by-step reasoning to solve grid puzzles: Where do LLMs falter? ArXiv preprint, abs/2407.14790.
- Wang et al. (2024a) Ke Wang, Houxing Ren, Aojun Zhou, Zimu Lu, Sichun Luo, Weikang Shi, Renrui Zhang, Linqi Song, Mingjie Zhan, and Hongsheng Li. 2024a. Mathcoder: Seamless code integration in LLMs for enhanced mathematical reasoning. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024.
- Wang et al. (2023a) Lei Wang, Wanyu Xu, Yihuai Lan, Zhiqiang Hu, Yunshi Lan, Roy Ka-Wei Lee, and Ee-Peng Lim. 2023a. Plan-and-Solve Prompting: Improving zero-shot Chain-of-Thought reasoning by large language models. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 2609–2634, Toronto, Canada.
- Wang et al. (2024b) Peiyi Wang, Lei Li, Liang Chen, Zefan Cai, Dawei Zhu, Binghuai Lin, Yunbo Cao, Lingpeng Kong, Qi Liu, Tianyu Liu, and Zhifang Sui. 2024b. Large language models are not fair evaluators. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pages 9440–9450, Bangkok, Thailand.
- Wang et al. (2024c) Weiqi Wang, Tianqing Fang, Chunyang Li, Haochen Shi, Wenxuan Ding, Baixuan Xu, Zhaowei Wang, Jiaxin Bai, Xin Liu, Cheng Jiayang, Chunkit Chan, and Yangqiu Song. 2024c. CANDLE: Iterative conceptualization and instantiation distillation from large language models for commonsense reasoning. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, pages 2351–2374, Bangkok, Thailand.
- Wang et al. (2023b) Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V. Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. 2023b. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations, Kigali, Rwanda.
- Wei et al. (2022) Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. Chain-of-Thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems, New Orleans, LA, USA.
- Xie et al. (2023) Yuxi Xie, Kenji Kawaguchi, Yiran Zhao, James Xu Zhao, Min-Yen Kan, Junxian He, and Michael Qizhe Xie. 2023. Self-evaluation guided beam search for reasoning. In Proceedings of the Annual Conference on Neural Information Processing Systems, New Orleans, LA, USA.
- Xu et al. (2024) Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. 2024. Faithful logical reasoning via Symbolic Chain-of-Thought. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pages 13326–13365, Bangkok, Thailand.
- Yao et al. (2023) Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. 2023. Tree of Thoughts: Deliberate problem solving with large language models. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems, New Orleans, LA, USA.
- Yu et al. (2020) Weihao Yu, Zihang Jiang, Yanfei Dong, and Jiashi Feng. 2020. Reclor: A reading comprehension dataset requiring logical reasoning. In 8th International Conference on Learning Representations.
- Zhang et al. (2023) Yifan Zhang, Jingqin Yang, Yang Yuan, and Andrew Chi-Chih Yao. 2023. Cumulative reasoning with large language models. ArXiv preprint, abs/2308.04371.
- Zhao et al. (2023) Wayne Xin Zhao, Kun Zhou, Junyi Li, Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, Yifan Du, Chen Yang, Yushuo Chen, Zhipeng Chen, Jinhao Jiang, Ruiyang Ren, Yifan Li, Xinyu Tang, Zikang Liu, Peiyu Liu, Jian-Yun Nie, and Ji-Rong Wen. 2023. A survey of large language models. ArXiv preprint, abs/2303.18223.
- Zhou et al. (2023) Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc V. Le, and Ed H. Chi. 2023. Least-to-Most prompting enables complex reasoning in large language models. In The Eleventh International Conference on Learning Representations, Kigali, Rwanda.
## Appendix A Logical Grammar
Facts: A fact is an assertion about specific individuals in the domain. It involves a predicate applied to constants (not variables) and states that a particular relationship holds between these individuals. For example, $\text{Sees}(\text{Jack},\text{Tom},\text{True})$ asserts Jack sees Tom.
Rules: A rule delineates a logical relationship between predicates and forms an integral component of the domain’s terminological knowledge. These rules typically incorporate variables and are universally quantified, ensuring their applicability across all relevant instances within the domain. Rules can involve logical connectors such as "and" ( $\land$ ), "or" ( $\lor$ ), "either…or…" (exclusive or, $\oplus$ ), and "not" ( $\neg$ ), appearing on both sides of the implication ( $\rightarrow$ ) or biconditional ( $\leftrightarrow$ ) operators. For instance, the rule
$$
\forall x,y\left(\text{Sees}(x,y)\rightarrow\text{Knows}(x,y)\right)
$$
asserts that for all individuals $x$ and $y$ , if $x$ sees $y$ , then $x$ knows $y$ .
Query: A query is a fact that needs to be proven based on the given facts and rules.
## Appendix B Three potential situations for searching complement
When searching for a complementary clause during the resolution process, three potential situations may arise.
- If exactly one complementary clause is found the resolution will be directly implemented.
- If multiple complementary clauses are identified, we prioritize the shorter clauses, while saving the remaining clauses as backup options. In cases where the current reasoning path cannot find any further complementary clauses before reaching the predefined maximum number of iterations, we will backtrack and attempt to use these backup clauses.
- If no complementary clause is found initially, we will backtrack to the backup list. Should the backup list also be exhausted, we will conclude the reasoning process by determining the result as "No contradiction found."
This approach ensures a structured and efficient search and resolution process, while also accounting for cases where multiple or no complementary clauses are found, improving overall search robustness.
## Appendix C Conjunctive Normal Form
Conjunctive Normal Form (CNF) is a standardized way of expressing logical statements in Boolean logic. In CNF, a formula is composed of a conjunction (AND, denoted as $\land$ ) of clauses, where each clause is a disjunction (OR, denoted as $\lor$ ) of literals. A literal is either a variable or its negation. For example, the logical statement $(A\lor\neg B)\land(C\lor D)$ is in CNF. Each group within the parentheses is a clause, and the entire expression is the conjunction of these clauses. The reason we need logical statements to be in CNF to conduct resolution is that resolution is a fundamental inference rule in automated theorem proving. It works by finding pairs of clauses where one contains a literal and the other contains its negation. These pairs can then be combined to eliminate the opposing literals, simplifying the overall logical expression. Since CNF breaks down complex statements into smaller, manageable components of ANDs and ORs, it allows the resolution rule to systematically and efficiently simplify or refute logical expressions, thus enabling automated reasoning systems to solve problems.
## Appendix D Dataset Specifications
ProntoQA is a synthetic dataset designed to assess models’ deductive reasoning abilities. For our evaluation, we use the most difficult 5-hop subset. Each question in this dataset requires verifying whether a given claim is "True" or "False" based on the provided premises. The dataset focuses on basic logical relationships. For instance, given "X is Y", "Y is Z", determining whether "X is Z".
ProofWriter is a popular dataset for logical deductive reasoning. The dataset has five subsets with different reasoning depths (from 1 to 5). We use the hardest depth-5 subset for evaluation. And the context in this dataset contains more challenging logical relationships such as the combination of "and" and "or".
LogicNLI is a challenging NLI-style dataset that effectively disentangles the target logical reasoning from commonsense inference. In addition to common logical relationships such as "and" and "or", it presents the most difficult relationships among the three datasets, such as "either…or…", "vice versa", and "if and only if".
The test sizes are 500 for ProntoQA, 600 for ProofWriter, and 300 for LogicNLI, respectively.
## Appendix E Evaluation on Real-world Dataset
| CoT Aristotle | 75.0 76.5 | 65.6 31.2 |
| --- | --- | --- |
Table 4: Performance on Real-world’s Benchmark
The ability to solve real-world problems is important, as it reflects a model’s applicability beyond synthetic or constrained settings. Numerous benchmarks Han et al. (2022); Patel et al. (2024); Liu et al. (2023); Parmar et al. (2024); Liu et al. (2020); Yu et al. (2020); Tyagi et al. (2024) have been introduced to evaluate this capability by incorporating tasks that require implicit reasoning, background knowledge, and commonsense understanding.
We include an evaluation on real-world datasets FOLIO Han et al. (2022) and LogiQA Liu et al. (2020), to provide a deeper understanding of Aristotle. As shown in Table 4, Aristotle’s performance is suboptimal. This is primarily due to its design: it operates on explicitly stated premises and deliberately avoids relying on unstated assumptions or external background knowledge. However, real-world scenarios frequently depend on such implicit information and commonsense reasoning, making these capabilities essential for robust performance.
While Aristotle promotes clarity and precision in logical inference, it may not fully capture the complexities inherent in real-world tasks—a limitation we have acknowledged in the main paper. Notably, Aristotle’s performance on LogiQA is significantly worse than on FOLIO. Our qualitative analysis reveals that this discrepancy stems from LogiQA’s greater reliance on commonsense knowledge and implicit assumptions, which makes it less compatible with Aristotle’s strictly premise-driven reasoning approach.
To address this, our plan is to incorporate external knowledge to better handle such scenarios in future work. For instance, information retrieval from the internet or commonsense knowledge graphs could supplement the explicit premises with the necessary implicit knowledge for reasoning. This integration would enable our method to leverage background information that is not explicitly provided, improving its applicability and performance in solving real-world tasks.
## Appendix F Error Analysis
Here, we present a more detailed error analysis.
### F.1 False Contradiction
False contradiction refers to when the method identifies a contradiction when none should exist, leading to an incorrect final answer. This issue often arises in cases where the ground truth of a problem is false. For example, when the ground truth is false, we should find a contradiction when reasoning from the negation of the statement and no contradiction when reasoning from the original statement, as outlined in the equation 1.
However, our method sometimes finds a contradiction even when reasoning from the original statement, altering the final answer and producing errors. This should be due to the way datasets are constructed. When the ground truth is false, for instance, the dataset may be built such that the false statement is provable, but the construction process might fail to ensure that the true statement is not provable. This oversight results in both the true and false values being provable, making the problem self-contradictory. This situation occurs more frequently when the ground truth is either true or false, suggesting that the dataset did not fully account for the exclusive relationship between proving one value and excluding the other.
In an ideal dataset construction where the ground truth is true or false, the premises should only allow for the ground truth to be provable, while any other possible answers should be logically excluded. That is, if a statement is provably true, it should be impossible to prove its negation, and vice versa. Ensuring this exclusivity is crucial for logical consistency.
That said, it’s important to note that these False Contradictions represent only a small portion of the overall dataset. While this issue can affect some instances, it doesn’t significantly undermine the dataset’s overall effectiveness for testing reasoning models.
### F.2 Resolver Instantiation Error
An instantiation error occurs when a resolver incorrectly substitutes a variable, leading to an inaccurate conclusion. For example, given two clauses: $Smart(Gary,False)$ and $Smart(Gary,True)\lor Nice(x,False)$ , the correct resolution would recognize that $Smart(Gary,False)$ directly complements $Smart(Gary,True)$ , resulting in the simplified clause $Nice(x,False)$ without needing to instantiate ‘x‘. However, if the resolver mistakenly instantiates "x" as "Gary," the clause changes to $Nice(Gary,False)$ , which is more specific than necessary.
This error restricts the generality of the conclusion, as the correct clause $Nice(x,False)$ is intended to apply to any individual, not just "Gary." Such improper instantiation can lead to faulty reasoning in subsequent steps, where conclusions might be incorrectly drawn because the reasoning process has been prematurely narrowed to a specific case. Ensuring that instantiation only occurs when necessary can help prevent these errors and maintain the validity of logical deductions.
## Appendix G Baselines
Here we illustrate the details of each baseline.
#### Naive Prompting
Naive Prompting refers to a basic prompting technique where a model is given a question or task without any complex instructions or intermediate steps. The model is expected to output a direct answer based on its existing knowledge. In this approach, the reasoning process is implicit, and the model simply leverages its pre-trained knowledge to respond without additional structured reasoning or step-by-step guidance.
#### Chain-of-Thought (CoT)
Chain-of-Thought (CoT) prompting is a more advanced prompting strategy that encourages the model to generate intermediate reasoning steps before arriving at a final answer. Instead of asking the model for an immediate response, the prompt guides the model to break down the reasoning process into smaller, logical steps. This allows the model to engage in more thoughtful problem-solving and often leads to better performance on tasks requiring multi-step reasoning Wei et al. (2022).
#### Chain-of-Thought with Self-Consistency (CoT-SC)
Chain-of-Thought with Self-Consistency (CoT-SC) improves upon the standard CoT method by running the chain-of-thought reasoning process multiple times independently. Instead of producing just one reasoning chain per query, the model generates multiple chains for the same task. After running these different reasoning processes, the final answer is determined by applying majority voting on the outputs. This ensures that the model selects the answer that is most consistent across multiple reasoning attempts, which helps reduce variability and errors caused by randomness or incorrect intermediate steps in any single chain Wang et al. (2023b).
#### Cumulative Reasoning (CR)
Cumulative Reasoning builds on the idea that reasoning can be improved over successive iterations. The model does not simply reach a conclusion in one step, but rather, the reasoning evolves across multiple stages or passes. In this process, intermediate results are used as building blocks for the final solution, allowing the model to accumulate information and refine its reasoning step by step Zhang et al. (2023).
#### DetermLR
DetermLR is a reasoning approach that rethinks the process as an evolution from indeterminacy to determinacy. It categorizes premises into determinate (clear) and indeterminate (uncertain) types, guiding models to convert indeterminate data into determinate insights. The approach uses quantitative methods to prioritize relevant premises and employs reasoning memory to store and retrieve historical reasoning paths. This helps streamline the reasoning process, progressively refining the model’s understanding to produce more determinate and accurate conclusions Sun et al. (2024).
#### Tree-of-Thought (ToT)
Tree-of-Thought (ToT) is a framework that uses a tree-like structure for reasoning. Instead of generating a single chain of thought, the model explores multiple reasoning pathways in parallel, branching out into different possible solutions. The tree structure allows the model to evaluate and prune different paths, keeping only the most promising routes to reach the correct solution. This approach is particularly useful for problems where multiple reasoning paths can lead to the answer, allowing for exploration and selection of the best path Yao et al. (2023).
#### SymbCoT
SymbCoT integrates symbolic expressions and rules into the chain-of-thought (CoT) process. It translates natural language input into symbolic representations, allowing the model to reason based on these symbolic expressions. The LLM then applies symbolic rules to process and analyze the information, enhancing its ability to handle tasks that require formal reasoning and structured problem-solving Xu et al. (2024).
#### Logic-LM
Logic-LM translates natural language input into a symbolic format and then applies a rule-based logical engine to perform reasoning. This approach leverages formal logic rules to process and analyze the symbolic representation, enabling more structured and precise reasoning, particularly for tasks that require strict logical inferences Pan et al. (2023).
## Appendix H Full Algorithm
Input: Premises $P$ , Question Statement $S$ , LLM $p_{\theta}$ , Translator $T()$ , Decomposer $D()$ , Search Router $SR()$ , Resolver $R()$ , Search Round Limit $S$
$P_{t},S_{t}\leftarrow T(P,S)$ ;
// Translate the given premises and statement
$P_{n},S_{n}\leftarrow D(P_{t},S_{t})$ ;
// Decompose the translated premises and statement
$C_{\text{current\_list}}\leftarrow[S_{n},\neg S_{n}]$ ;
// Initiate search with $S_{n}$ and its negation
1 $Search\_round\leftarrow 0$ ;
2
3 foreach $C_{\text{current}}$ in $C_{\text{current\_list}}$ do
4 while $Search\_round<S$ do
$C_{\text{searched\_list}}\leftarrow SR(C_{\text{current}},P_{n})$ ;
// Search for complementary clause
5 $num\_searched\_C\leftarrow\text{len}(C_{\text{searched\_list}})$ ;
6
7 if $num\_searched\_C>=1$ then
8 $C_{\text{searched}}\leftarrow C_{\text{searched\_list}}[0]$ ;
9
10 else
11 $C_{\text{searched}}\leftarrow C_{\text{searched\_list}}.\text{pop}(0)$ ;
12
13 end if
14
$cache\leftarrow\{P_{n}:C_{\text{searched\_list}}\}$ ;
// If more than one $C_{\text{current}}$ , save in $cache$
15
16 if $num\_searched\_C==0$ then
17 if $\text{cache}[C_{\text{current}}]$ is not empty then
$C_{\text{current}}\leftarrow\text{next}(\text{iter}(\text{cache}))$ ;
// If no $C_{c}urrent$ found, search from $cache$
18 $C_{\text{searched}}\leftarrow\text{cache}[C_{\text{current}}].\text{pop}(0)$ ;
19
20 end if
21 else
22 if Start from $S_{n}$ then
$D_{S_{n}}\leftarrow P\not\vdash\neg S$ ;
// If $cache$ is empty, make conclusion
23
24 end if
25 if Start from $\neg S_{n}$ then
26 $D_{\neg S_{n}}\leftarrow P\not\vdash S$ ;
27
28 end if
29 break;
30
31 end if
32
33 end if
34
35 $C_{\text{resolved}}\leftarrow R(C_{\text{current}},C_{\text{searched}})$ ;
36 if $C_{\text{resolved}}==\text{`Contradiction'}$ then
37 if Start from $S_{n}$ then
$D_{S_{n}}\leftarrow P\vdash\neg S$ ;
// If contradiction is found, make conclusion
38 ;
39 end if
40 if Start from $\neg S_{n}$ then
41 $D_{\neg S_{n}}\leftarrow P\vdash S$ ;
42
43 end if
44 break;
45
46 end if
47 else
$P_{n}\leftarrow P_{n}\cup\{C_{\text{resolved}}\}$ ;
// Append $C_{\text{resolved}}$ on $P_{n}$
48
49 end if
50 $C_{\text{current}}\leftarrow C_{\text{resolved}}$ ;
51
52 end while
53 if Start from $S_{n}$ then
$D_{S_{n}}\leftarrow P\not\vdash\neg S$ ;
// If no contradiction found and reach max iterations, make conclusion
54
55 end if
56 if Start from $\neg S_{n}$ then
57 $D_{\neg S_{n}}\leftarrow P\not\vdash S$ ;
58
59 end if
60
61 end foreach
Algorithm 1 Methodology
## Appendix I Case Study
Given the premises, we need to determine whether the question statement $S$ "Dave is not nice" is true/false/unknown/self-contradictory. We first start the first reasoning path from $C_{\text{current}}$ = $S_{n}$ . $C_{\text{complement}}$ is the complementary clause found by the Search Router from $P_{n}$ .
Logical Resolution Steps
Translated and Decomposed Premises $P_{n}$ : 1.
If someone is green then they are nice ::: $\forall x\left(\text{Green}(x,\text{False})\lor\text{Nice}(x,\text{True})\right)$ 2.
If someone is smart then they are green ::: $\forall x\left(\text{Smart}(x,\text{False})\lor\text{Green}(x,\text{True})\right)$ 3.
Dave is smart ::: $\text{Smart}(\text{Dave},\text{True})$ Question Statement $S_{n}$ : Dave is not nice ::: Nice(Dave, False) $C_{\text{current}}:\quad\text{Nice}(\text{Dave},\text{False})$ Resolution Steps: 1.
First Resolution:
$\text{Resolve}\left(C_{\text{current}}=\text{Nice}(\text{Dave},\text{False}),\ C_{\text{complement}}=\forall x\left(\text{Green}(x,\text{False})\lor\text{Nice}(x,\text{True})\right)\right)$
•
Instantiate $C_{\text{complement}}$ for $x=\text{Dave}$ :
$\text{Green}(\text{Dave},\text{False})\lor\text{Nice}(\text{Dave},\text{True})$ •
Resolve with $C_{\text{current}}=\text{Nice}(\text{Dave},\text{False})$ :
$\displaystyle\text{Nice}(\text{Dave},\text{False})$ and $\displaystyle\text{Green}(\text{Dave},\text{False})\lor\text{Nice}(\text{Dave},\text{True})$ •
Since $\text{Nice}(\text{Dave},\text{False})$ contradicts $\text{Nice}(\text{Dave},\text{True})$ , the new resolved clause is:
$C_{\text{resolved}}=\text{Green}(\text{Dave},\text{False})$ •
Update $C_{\text{current}}$ to $C_{\text{resolved}}$ :
$C_{\text{current}}=C_{\text{resolved}}=\text{Green}(\text{Dave},\text{False})$ 2.
Second Resolution:
$\text{Resolve}\left(C_{\text{current}}=\text{Green}(\text{Dave},\text{False}),\ C_{\text{complement}}=\forall x\left(\text{Smart}(x,\text{False})\lor\text{Green}(x,\text{True})\right)\right)$
•
Instantiate $C_{\text{complement}}$ for $x=\text{Dave}$ :
$\text{Smart}(\text{Dave},\text{False})\lor\text{Green}(\text{Dave},\text{True})$ •
Resolve with $C_{\text{current}}=\text{Green}(\text{Dave},\text{False})$ :
$\displaystyle\text{Green}(\text{Dave},\text{False})$ and $\displaystyle\text{Smart}(\text{Dave},\text{False})\lor\text{Green}(\text{Dave},\text{True})$ •
Since $\text{Green}(\text{Dave},\text{False})$ contradicts $\text{Green}(\text{Dave},\text{True})$ , the new resolved clause is:
$C_{\text{resolved}}=\text{Smart}(\text{Dave},\text{False})$ •
Update $C_{\text{current}}$ to $C_{\text{resolved}}$ :
$C_{\text{current}}=C_{\text{resolved}}=\text{Smart}(\text{Dave},\text{False})$ 3.
Third Resolution:
$\text{Resolve}\left(C_{\text{current}}=\text{Smart}(\text{Dave},\text{False}),\ C_{\text{complement}}=\text{Smart}(\text{Dave},\text{True})\right)$
•
Resolve $\text{Smart}(\text{Dave},\text{False})$ with $\text{Smart}(\text{Dave},\text{True})$ :
$\displaystyle\text{Smart}(\text{Dave},\text{False})$ and $\displaystyle\text{Smart}(\text{Dave},\text{True})$ •
Since $\text{Smart}(\text{Dave},\text{False})$ contradicts $\text{Smart}(\text{Dave},\text{True})$ , the final resolved clause is:
$C_{\text{resolved}}=\text{Contradiction}$
Conclusion: $D_{S_{n}}$ = $P\vdash\neg S$
We then start the second reasoning path from $C_{\text{current}}$ = $\neg S_{n}$ .
Logical Resolution Steps
Translated and Decomposed Premises $P_{n}$ : 1.
If someone is green then they are nice ::: $\forall x\left(\text{Green}(x,\text{False})\lor\text{Nice}(x,\text{True})\right)$ 2.
If someone is smart then they are green ::: $\forall x\left(\text{Smart}(x,\text{False})\lor\text{Green}(x,\text{True})\right)$ 3.
Dave is smart ::: $\text{Smart}(\text{Dave},\text{True})$ Question Statement $S_{n}$ : Dave is not nice ::: Nice(Dave, False) $C_{\text{current}}=\neg S_{n}=\text{Nice}(\text{Dave},\text{True})$ Resolution Steps: 1.
First Resolution:
No complementary clause was found from the given premises, thus we directly conclude "No contradiction found"
Conclusion: $D_{\neg S_{n}}$ = $P\not\vdash S$
Since we get: $D_{S_{n}}$ = $P\vdash\neg S$ and $D_{\neg S_{n}}$ = $P\not\vdash S$ from two reasoning paths correspondingly, according to Eq. (1), the final answer is False.
## Appendix J Full Prompting of Each Module
### J.1 ProntoQA
Translation
Task Description: You are given a problem description and a question. The task is to: 1.
Define all the predicates in the problem. 2.
Parse the problem into logic rules based on the defined predicates. 3.
Write all the facts mentioned in the problem. 4.
Parse the question into the logic form. Premises $P$ : •
Each jompus is fruity. Every jompus is a wumpus. Every wumpus is not transparent. Wumpuses are tumpuses. Tumpuses are mean. Tumpuses are vumpuses. Every vumpus is cold. Each vumpus is a yumpus. Yumpuses are orange. Yumpuses are numpuses. Numpuses are dull. Each numpus is a dumpus. Every dumpus is not shy. Impuses are shy. Dumpuses are rompuses. Each rompus is liquid. Rompuses are zumpuses. Alex is a tumpus. Statement $S$ : •
True or false: Alex is not shy. Facts (included in $P_{t}$ ): •
$Tumpuses(Alex)$ : Alex is a tumpus. •
(… more facts …) Rules (included in $P_{t}$ ): •
$Jompus(x)\Rightarrow Fruity(x)$ : Each jompus is fruity. •
(… more rules …) Translated Query $S_{t}$ : •
$Shy(Alex,False)$ ::: Alex is not shy
Decomposition
Task Description: You are given a problem description and a question. The task is to: 1.
Given the premises and conjecture in logical form, decompose the logical statements using normalization and skolemization. 2.
Normalization: Convert each premise and conjecture into Prenex Normal Form (PNF), then into Conjunctive Normal Form (CNF). 3.
Skolemization: Eliminate existential quantifiers by introducing Skolem constants or functions. Premises $P_{t}$ : •
$Jompus(x,True)\rightarrow Shy(x,False)$ •
$Jompus(x,True)\rightarrow Yumpus(x,True)$ •
(…more premises… ) Query $S_{t}$ : •
$Sour(Max,True)$ Decomposed Premises $P_{n}$ : •
1. $\neg Jompus(x,True)\lor Shy(x,False)$ •
2. $(\neg Jompus(x,True)\lor Yumpus(x,True)$ •
(… additional decomposed premises …) Query $S_{n}$ : •
$Sour(Max,True)$
Resolve
Task Description: You are given a problem description and a question. The task is to: 1.
Check for Complementary/Contradictory Terms. Two terms are contradictory if they share the same predicate and arguments but differ in boolean value (True vs. False). 2.
If contradictory terms are found, apply the resolution rule: From $(P(x,True)\lor Q(x,True))$ and $(P(x,False)\lor M(x,True))$ , derive $Q(x,True)\lor M(x,True)$ . 3.
If the resolution leads to an empty clause or direct contradiction, then output "Contradiction". Otherwise output the new clause after resolution. Example: Given Clauses ( $C_{\text{current}}$ and $C_{\text{complement}}$ ) •
$Difficult(Bradley,True)\lor Known(x,False)$ •
$Difficult(x,False)\lor Embarrassed(x,True)\lor Colorful(x,False)$ Resolved $C_{\text{resolved}}$ : •
$Known(x,False)\lor Embarrassed(Bradley,True)\lor Colorful(Bradley,False)$ (…more examples…)
### J.2 ProofWriter
Translation
Task Description: You are given a problem description and a question. The task is to: 1.
Define all the predicates in the problem. 2.
Parse the problem into logic rules based on the defined predicates. 3.
Write all the facts mentioned in the problem. 4.
Parse the question into the logic form. Premises $P$ : •
Anne is quiet. Erin is furry. Erin is green. Fiona is furry. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is white. Harry is furry. Harry is quiet. Harry is white. Young people are furry. If Anne is quiet then Anne is red. Young, green people are rough. If someone is green then they are white. If someone is furry and quiet then they are white. If someone is young and white then they are rough. All red people are young. Statement $S$ : •
Is the following statement true, false, or unknown? Anne is white. Facts (included in $P_{t}$ ): •
$Quite(Anne,True)$ : Anne is quiet. •
(… More facts …) Rules (included in $P_{t}$ ): •
$Young(x,True)\Rightarrow Furry(x,True)$ : Young people are furry. •
(… More rules …) Query $S_{t}$ : •
White(Anne, True) ::: Anne is white.
Decomposition
Task Description: You are given a problem description and a question. The task is to: 1.
Given the premises and conjecture in logical form, decompose the logical statements using normalization and skolemization. 2.
Normalization: Convert each premise and conjecture into Prenex Normal Form (PNF), then into Conjunctive Normal Form (CNF). 3.
Skolemization: Eliminate existential quantifiers by introducing Skolem constants or functions. Premises $P_{t}$ : •
$Quite(Anne,True)$ : Anne is quiet. •
$Young(x,True)\Rightarrow Furry(x,True)$ : Young people are furry. •
(…more premises… ) Query $S_{t}$ : •
White(Anne, True) ::: Anne is white. Decomposed Premises $P_{n}$ : •
1. $Quite(Anne,True)$ •
2. $Young(x,False)\lor Furry(x,True)$ •
(… additional decomposed premises …) Query $S_{n}$ : •
$White(Anne,True)$
Resolve
Task Description: You are given a problem description and a question. The task is to: 1.
Check for Complementary/Contradictory Terms. Two terms are contradictory if they share the same predicate and arguments but differ in boolean value (True vs. False). 2.
If contradictory terms are found, apply the resolution rule: From $(P(x,True)\lor Q(x,True))$ and $(P(x,False)\lor M(x,True))$ , derive $Q(x,True)\lor M(x,True)$ . 3.
If the resolution leads to an empty clause or direct contradiction, then output "Contradiction". Otherwise output the new clause after resolution. Example: Given Clauses ( $C_{\text{current}}$ and $C_{\text{complement}}$ ) •
$Difficult(Bradley,True)\lor Known(x,False)$ •
$Difficult(x,False)\lor Embarrassed(x,True)\lor Colorful(x,False)$ Resolved $C_{\text{resolved}}$ : •
$Known(x,False)\lor Embarrassed(Bradley,True)\lor Colorful(Bradley,False)$ (…more examples…)
### J.3 LogicNLI
Translation
Task Description: You are given a problem description and a question. The task is to: 1.
Define all the predicates in the problem. 2.
Parse the problem into logic rules based on the defined predicates. 3.
Write all the facts mentioned in the problem. 4.
Parse the question into the logic form. 5.
Please make sure to differentiate ’or’ and ’either…or…’. For ’or’, you should translate it with the inclusive ’or’ ( $\lor$ ) operator. For ’either…or…’, you should translate it with the ’exclusive or’ ( $\oplus$ ) operator. 6.
Please be careful when translating clauses with words "equivalent", "vice versa" and "if and only if". Make sure you use the biconditional " $\leftrightarrow$ " in those translations. Premises $P$ : •
Medwin is doubtful. Roberto is not bitter. Roberto is not grieving. If someone is not bitter, then he is not grieving. Medwin being not sociable implies that Medwin is not pure. If there is someone who is either not pure or not doubtful, then Lynda is not grieving. Statement $S$ : •
Bernard is not bitter. Facts (included in $P_{t}$ ): •
$Doubtful(Medwin,True)$ ::: Medwin is doubtful. •
(… More facts …) Rules (included in $P_{t}$ ): •
$Bitter(x,False)\Rightarrow Grieving(x,False)$ : If someone is not bitter, then he is not grieving. •
(… More rules …) Query $S_{t}$ : •
Bitter(Bernard, False) ::: Bernard is not bitter.
Decomposition
Task Description: You are given a problem description and a question. The task is to: 1.
Given the premises and conjecture in logical form, decompose the logical statements using normalization and skolemization. 2.
Normalization: Convert each premise and conjecture into Prenex Normal Form (PNF), then into Conjunctive Normal Form (CNF). 3.
Skolemization: Eliminate existential quantifiers by introducing Skolem constants or functions. Premises $P_{t}$ : •
$Doubtful(Medwin,True)$ ::: Medwin is doubtful. •
$Bitter(x,False)\Rightarrow Grieving(x,False)$ : If someone is not bitter, then he is not grieving. •
(…more premises… ) Query $S_{t}$ : •
$Bitter(Bernard,False)$ ::: Bernard is not bitter. Decomposed Premises $P_{n}$ : •
1. $Doubtful(Medwin,True)$ •
2. $Bitter(x,True)\lor Grieving(x,False)$ •
(… additional decomposed premises …) Query $S_{n}$ : •
$Bitter(Bernard,False)$
Resolve
Task Description: You are given a problem description and a question. The task is to: 1.
Check for Complementary/Contradictory Terms. Two terms are contradictory if they share the same predicate and arguments but differ in boolean value (True vs. False). 2.
If contradictory terms are found, apply the resolution rule: From $(P(x,True)\lor Q(x,True))$ and $(P(x,False)\lor M(x,True))$ , derive $Q(x,True)\lor M(x,True)$ . 3.
If the resolution leads to an empty clause or direct contradiction, then output "Contradiction". Otherwise output the new clause after resolution. Example: Given Clauses ( $C_{\text{current}}$ and $C_{\text{complement}}$ ) •
$Difficult(Bradley,True)\lor Known(x,False)$ •
$Difficult(x,False)\lor Embarrassed(x,True)\lor Colorful(x,False)$ Resolved $C_{\text{resolved}}$ : •
$Known(x,False)\lor Embarrassed(Bradley,True)\lor Colorful(Bradley,False)$ (…more examples…)