# 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
## Bar Chart: Performance Comparison of ToT vs. Ours
### Overview
The image presents a bar chart comparing the performance of two methods, "ToT" and "Ours," across two metrics: "Error Rate (%)" and "Reasoning Steps." The chart is divided into two sections, one for each metric. Each section displays the values for both methods as vertical bars, with numerical values displayed above each bar. Arrows indicate the difference between the "ToT" and "Ours" values.
### Components/Axes
* **Legend:** Located at the top of the chart.
* Blue bar: "ToT"
* Red bar: "Ours"
* **Left Chart:**
* Y-axis: "Error Rate (%)", with scale markings at 0, 10, 20, and 30.
* X-axis: Categorical, with two categories: "SE" and "RE".
* **Right Chart:**
* Y-axis: "Reasoning Steps", with scale markings at 0, 10, 20, and 30.
* X-axis: Implicitly categorical, with one category.
### Detailed Analysis
**Left Chart: Error Rate (%)**
* **SE (leftmost data):**
* ToT (blue bar): Error Rate of 15.0%
* Ours (red bar): The difference between ToT and Ours is -11.1%. Therefore, the Error Rate for Ours is approximately 15.0 - 11.1 = 3.9%
* **RE (rightmost data):**
* ToT (blue bar): Error Rate of 28.4%
* Ours (red bar): The difference between ToT and Ours is -28.0%. Therefore, the Error Rate for Ours is approximately 28.4 - 28.0 = 0.4%
**Right Chart: Reasoning Steps**
* ToT (blue bar): Reasoning Steps of 24.6
* Ours (red bar): The difference between ToT and Ours is -12.9. Therefore, the Reasoning Steps for Ours is approximately 24.6 - 12.9 = 11.7
### Key Observations
* In both metrics ("Error Rate" for SE and RE, and "Reasoning Steps"), "Ours" consistently outperforms "ToT," as indicated by the negative differences (downward arrows).
* The reduction in "Error Rate" is more significant for "RE" (-28.0%) compared to "SE" (-11.1%).
* The reduction in "Reasoning Steps" is -12.9.
### Interpretation
The data suggests that the "Ours" method is more effective than the "ToT" method, resulting in lower error rates and fewer reasoning steps. The substantial reduction in error rate for "RE" indicates that "Ours" is particularly advantageous in this category. The reduction in reasoning steps suggests that "Ours" is also more efficient. Overall, the chart provides evidence that "Ours" is a superior approach compared to "ToT" in the contexts evaluated.
</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
## Diagram: Reasoning Trajectories for Logical Deduction
### Overview
The image presents a diagram illustrating a reasoning process to determine the truth value of a question based on given premises. It outlines the steps involved in translating, decomposing, searching, resolving, and concluding an answer. The diagram is divided into three main steps: Search Initialization, Search and Resolve, and Conclude Answer, with a parallel "Reasoning Trajectories" section showing the detailed steps.
### Components/Axes
* **Raw Input:** Contains the initial premises and the question to be answered.
* **Premise (P):** "If people are patient, then they are nice. If people are smart, then they are patient. Dave is Smart."
* **Question (S):** "Dave is nice. (True/False/Unknown/Self-Contradiction)"
* **Translator:** A component that translates the raw input.
* **Decomposer:** A component that decomposes the translated input.
* **Translated and Decomposed:** The result of translation and decomposition.
* **Premises (Pn):**
1. Patient(x, False) ∨ Nice(x, True)
2. Smart(x, False) ∨ Patient(x, True)
3. Smart(Dave, True)
* **Question (Sn):** Nice(Dave, True)
* **Initialization:** Sets up the initial states for the search.
* Sn: Nice(Dave, True)
* ¬Sn: Nice(Dave, False)
* **Search Router:** Routes the search based on available information.
* **Resolver:** Resolves clauses to derive new information.
* **Reasoning Complete?:** A decision point to determine if the reasoning process is complete.
* **Proof:** Indicates whether a contradiction or no contradiction is found.
* ¬Sn: Contradiction
* Sn: No contradiction
* **Final Answer:** The conclusion reached after the reasoning process.
* The answer is True.
* **Reasoning Trajectories:** Shows the step-by-step reasoning process.
* **Current Clause:** The current clause being considered.
* **Complementary Clause:** The clause used to resolve with the current clause.
* **Resolved Clause:** The result of resolving the current and complementary clauses.
### Detailed Analysis
**Step 1: Search Initialization**
* The process starts with the question "Nice(Dave, True)" and its negation "Nice(Dave, False)".
**Step 2: Search and Resolve**
* The "Search Router" directs the process based on the current clauses and premises.
* The "Resolver" attempts to resolve clauses to derive new information.
* The "Reasoning Trajectories" section shows the detailed steps:
* **Round 1:**
* Current Clause: ¬Sn: Nice(Dave, False)
* Complementary Clause: Patient(x, False) ∨ Nice(x, True)
* Resolved Clause: Patient(Dave, False)
* **Round 2:**
* Current Clause: Patient(Dave, False)
* Complementary Clause: Smart(x, False) ∨ Patient(x, True)
* Resolved Clause: Smart(Dave, False)
* **Round 3:**
* Current Clause: Smart(Dave, False)
* Complementary Clause: Smart(Dave, True)
* Resolved Clause: Contradiction!
* If a contradiction is found, the process moves to the "Proof" stage.
**Step 3: Conclude Answer**
* If a contradiction is found (¬Sn: Contradiction), the final answer is "True".
* If no contradiction is found (Sn: No contradiction), the final answer would be "False" (though this path isn't fully shown).
### Key Observations
* The diagram illustrates a logical deduction process using resolution.
* The "Reasoning Trajectories" section provides a detailed view of the steps involved in resolving clauses.
* The process aims to find a contradiction to prove the truth of the initial question.
### Interpretation
The diagram demonstrates a method for automated reasoning. It starts with premises and a question, translates and decomposes them into logical clauses, and then uses a resolution-based search to determine the truth value of the question. The "Reasoning Trajectories" section is crucial as it shows the step-by-step derivation of new clauses until a contradiction is found, which confirms the truth of the initial question. The diagram highlights the importance of logical deduction in artificial intelligence and knowledge representation. The process effectively shows how a computer can "think" through a problem and arrive at a logical conclusion.
</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
## Icon: Language Translation
### Overview
The image is an icon representing language translation. It features two overlapping shapes, one resembling a speech bubble containing a Chinese character, and the other resembling a document with the letter "A". Curved arrows indicate a bidirectional flow between the two.
### Components/Axes
* **Left Shape:** A white speech bubble with a light purple shadow, containing a dark gray Chinese character (文).
* **Right Shape:** A light blue document shape with a darker blue shadow, containing a dark gray letter "A".
* **Arrows:** Two dark gray curved arrows. One curves from the bottom of the speech bubble to the bottom of the document, and the other curves from the top of the document to the top of the speech bubble.
### Detailed Analysis
* The Chinese character (文) is positioned centrally within the speech bubble.
* The letter "A" is positioned centrally within the document shape.
* The arrows indicate a two-way process, suggesting translation from one language (represented by the Chinese character) to another (represented by the letter "A"), and vice versa.
### Key Observations
* The icon uses simple shapes and colors to convey the concept of language translation.
* The use of a Chinese character and the letter "A" suggests translation between Chinese and English, or more generally, between any two languages.
* The bidirectional arrows emphasize the two-way nature of translation.
### Interpretation
The icon effectively communicates the idea of language translation. The use of distinct linguistic symbols (Chinese character and the letter "A") clearly represents different languages. The arrows indicate the process of converting text from one language to another. The bidirectional nature of the arrows suggests that the translation can occur in either direction. This icon could be used in software, websites, or other contexts to indicate language translation features or services.
</details>
Translator and
<details>
<summary>figure/decomposer.png Details</summary>
### Visual Description
## Diagram: Basic Flowchart
### Overview
The image is a simple flowchart diagram. It consists of five rounded rectangles (nodes) connected by blue lines, indicating a hierarchical flow from top to bottom. The nodes are colored yellow, red, green, and blue.
### Components/Axes
* **Nodes:** Five rounded rectangles, each representing a step or element in the process.
* Top Node: Yellow
* Middle Row (left to right): Red, Green
* Bottom Row (left to right): Green, Yellow, Blue
* **Connectors:** Blue lines with rounded corners, indicating the direction of flow. The lines connect the top node to the two nodes in the middle row, and the two nodes in the middle row to the three nodes in the bottom row.
### Detailed Analysis
The flowchart starts with a single yellow node at the top. This node branches out to two nodes in the second level: a red node on the left and a green node on the right. From the red and green nodes, the flow continues to three nodes in the bottom row: a green node, a yellow node, and a blue node. The lines connecting the nodes are all the same color (blue) and thickness, suggesting a uniform relationship between the elements.
### Key Observations
* The diagram illustrates a hierarchical structure with a single starting point and multiple endpoints.
* The use of different colors for the nodes may indicate different categories or types of elements within the process.
* The flow is strictly top-down, with no loops or feedback mechanisms.
### Interpretation
The flowchart represents a basic process or decision tree. The yellow node at the top could represent an initial state or decision, which then leads to different paths represented by the red and green nodes. The bottom row of nodes could represent final outcomes or actions. The specific meaning of the diagram would depend on the context in which it is used. The different colors likely represent different categories or types of elements within the process.
</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
## Icon: Cartoon of a Man
### Overview
The image is a cartoon-style icon of a man with a beard and gray hair, wearing a white robe. The style is simple with thick black outlines and flat colors.
### Components/Axes
* **Head:** The man has a round face, gray hair, and a beard.
* **Eyes:** The eyes are represented by simple black ovals.
* **Robe:** He is wearing a white robe.
* **Outline:** Thick black outlines define the shapes.
* **Color Palette:** The colors are limited to skin tone, gray, white, and black.
### Detailed Analysis or ### Content Details
The man's face is a light skin tone. His hair and beard are gray. He is wearing a white robe. The image is a simple cartoon representation of a man, possibly intended to represent a historical figure or philosopher.
### Key Observations
The icon is stylized and simplified, focusing on key features like the beard and robe.
### Interpretation
The icon likely represents a historical figure, possibly a philosopher or scholar, given the beard and robe. The simple style makes it suitable for use as an icon in a user interface or other digital context. The lack of specific details makes it difficult to identify a particular individual.
</details>
Aristotle Architecture
We first formally define the logical reasoning task. Given a set of premises $P=\{p_{1},p_{2},...,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
## Icon: Language Translation
### Overview
The image is an icon representing language translation. It features two overlapping shapes, one resembling a speech bubble containing a Chinese character, and the other resembling a document with the letter "A". Curved arrows indicate a bidirectional flow between the two.
### Components/Axes
* **Left Shape:** A white speech bubble with a light purple shadow, containing a dark gray Chinese character (文).
* **Right Shape:** A light blue document shape with a darker blue shadow, containing a dark gray letter "A".
* **Arrows:** Two dark gray curved arrows. One curves from the bottom of the speech bubble to the bottom of the document, and the other curves from the top of the document to the top of the speech bubble.
### Detailed Analysis
* The Chinese character (文) is positioned centrally within the speech bubble.
* The letter "A" is positioned centrally within the document shape.
* The arrows indicate a two-way process, suggesting translation from one language (represented by the Chinese character) to another (represented by the letter "A"), and vice versa.
### Key Observations
* The icon uses simple shapes and colors to convey the concept of language translation.
* The use of a Chinese character and the letter "A" suggests translation between Chinese and English, or more generally, between any two languages.
* The bidirectional arrows emphasize the two-way nature of translation.
### Interpretation
The icon effectively communicates the idea of language translation. The use of distinct linguistic symbols (Chinese character and the letter "A") clearly represents different languages. The arrows indicate the process of converting text from one language to another. The bidirectional nature of the arrows suggests that the translation can occur in either direction. This icon could be used in software, websites, or other contexts to indicate language translation features or services.
</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
## Diagram: Basic Flowchart
### Overview
The image is a simple flowchart diagram. It consists of five rounded rectangles (nodes) connected by blue lines, indicating a hierarchical flow from top to bottom. The nodes are colored yellow, red, green, and blue.
### Components/Axes
* **Nodes:** Five rounded rectangles, each representing a step or element in the process.
* Top Node: Yellow
* Middle Row (left to right): Red, Green
* Bottom Row (left to right): Green, Yellow, Blue
* **Connectors:** Blue lines with rounded corners, indicating the direction of flow. The lines connect the top node to the two nodes in the middle row, and the two nodes in the middle row to the three nodes in the bottom row.
### Detailed Analysis
The flowchart starts with a single yellow node at the top. This node branches out to two nodes in the second level: a red node on the left and a green node on the right. From the red and green nodes, the flow continues to three nodes in the bottom row: a green node, a yellow node, and a blue node. The lines connecting the nodes are all the same color (blue) and thickness, suggesting a uniform relationship between the elements.
### Key Observations
* The diagram illustrates a hierarchical structure with a single starting point and multiple endpoints.
* The use of different colors for the nodes may indicate different categories or types of elements within the process.
* The flow is strictly top-down, with no loops or feedback mechanisms.
### Interpretation
The flowchart represents a basic process or decision tree. The yellow node at the top could represent an initial state or decision, which then leads to different paths represented by the red and green nodes. The bottom row of nodes could represent final outcomes or actions. The specific meaning of the diagram would depend on the context in which it is used. The different colors likely represent different categories or types of elements within the process.
</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 $∀ x\,(P(x)→ 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}}∈ 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}}∈ 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}}∈\left\{P_{n}\vdash\neg S_{n},P_{n}\not\vdash\neg S_{n}\right\}$ $D_{\neg S_{n}}∈\left\{P_{n}\vdash S_{n},P_{n}\not\vdash S_{n}\right\}$ $\blacktriangleright$ Output: $A∈\{\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
## Bar Chart: Accuracy Comparison of Different Models
### Overview
The image is a bar chart comparing the accuracy of different models on two datasets: ProofWriter and LogicNLI. The chart displays the accuracy (%) on the y-axis and the datasets on the x-axis. Different colored bars represent different model configurations: "Ours" (dark red), "w/o Decomposer" (medium red), "w/o Search Router" (light red), and "w/o Resolver" (palest red).
### Components/Axes
* **Y-axis:** Accuracy (%), with a scale from 30 to 90.
* **X-axis:** Two categories: ProofWriter and LogicNLI.
* **Legend:** Located at the bottom of the chart.
* Dark Red: Ours
* Medium Red: w/o Decomposer
* Light Red: w/o Search Router
* Pale Red: w/o Resolver
### Detailed Analysis
**ProofWriter Dataset:**
* **Ours (Dark Red):** 88.5%
* **w/o Decomposer (Medium Red):** 62.0%
* **w/o Search Router (Light Red):** 37.7%
* **w/o Resolver (Pale Red):** 47.1%
**LogicNLI Dataset:**
* **Ours (Dark Red):** 70.7%
* **w/o Decomposer (Medium Red):** 42.8%
* **w/o Search Router (Light Red):** 39.1%
* **w/o Resolver (Pale Red):** 57.5%
### Key Observations
* In both datasets, the "Ours" model achieves the highest accuracy.
* Removing the Decomposer has a more significant impact on accuracy than removing the Search Router in both datasets.
* Removing the Resolver has a more significant impact on accuracy for the LogicNLI dataset than the ProofWriter dataset.
### Interpretation
The bar chart demonstrates the performance of different model configurations on two datasets. The "Ours" model, presumably the complete model, consistently outperforms the configurations where components are removed. The relative impact of removing each component varies between the datasets, suggesting that the importance of each component is dataset-dependent. The "Decomposer" seems to be a more critical component than the "Search Router" for both datasets, as its removal leads to a larger drop in accuracy. The "Resolver" component seems to be more important for the LogicNLI dataset than for the ProofWriter dataset.
</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
## Scatter Plot: Accuracy vs. Number of Steps
### Overview
The image is a scatter plot comparing the accuracy (%) of different methods against the number of steps they require. The plot includes 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" with tick marks at 12, 16, 20, and 24.
* **Y-axis:** "Accuracy (%)" with tick marks at 65, 75, 85, and 95.
* **Data Series:**
* **Ours:** Represented by a red star.
* **DetermLR, CR, CoT-SC, ToT:** Represented by blue dots.
* **Gridlines:** Light gray gridlines are present in the background.
* **Legend:** The legend is implicitly defined by the labels next to each data point.
### Detailed Analysis
* **Ours:** The red star is located at approximately (12, 87).
* **DetermLR:** The blue dot is located at approximately (16, 79).
* **CR:** The blue dot is located at approximately (17, 72).
* **CoT-SC:** The blue dot is located at approximately (17, 70).
* **ToT:** The blue dot is located at approximately (24, 70).
### Key Observations
* "Ours" achieves the highest accuracy with the fewest number of steps.
* "ToT" requires the most steps but has a lower accuracy than "Ours" and "DetermLR".
* "CR" and "CoT-SC" have similar performance in terms of accuracy and number of steps.
### Interpretation
The scatter plot suggests that the "Ours" method is superior to the other methods in terms of accuracy and efficiency (number of steps). The other methods, "DetermLR", "CR", "CoT-SC", and "ToT", have lower accuracy and/or require more steps to achieve their respective accuracy levels. The plot highlights a trade-off between accuracy and the number of steps required, with "Ours" seemingly optimizing both.
</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
## Bar Chart: One-step Inference Accuracy
### Overview
The image is a bar chart comparing the "One-step Inference Accuracy" of two models, "ToT" (blue bars) and "Ours" (red bars), on two datasets: "ProofWriter" and "LogicNLI". The chart displays the accuracy in percentage for each model on each dataset. The chart also shows the increase in accuracy from "ToT" to "Ours" with an upward arrow and a percentage value.
### Components/Axes
* **Title:** One-step Inference Accuracy
* **Y-axis:** Accuracy (%) with scale markers at 60, 80, and 100.
* **X-axis:** Categorical axis with two categories: "ProofWriter" and "LogicNLI".
* **Legend:** Located at the bottom of the chart, indicating "ToT" (blue) and "Ours" (red).
### Detailed Analysis
* **ProofWriter:**
* ToT (blue): Accuracy is 74.0%.
* Ours (red): Accuracy is 99.7%.
* Increase from ToT to Ours: 25.7% (indicated by an upward arrow and the percentage value).
* **LogicNLI:**
* ToT (blue): Accuracy is 69.2%.
* Ours (red): Accuracy is 99.5%.
* Increase from ToT to Ours: 30.3% (indicated by an upward arrow and the percentage value).
### Key Observations
* "Ours" model significantly outperforms "ToT" on both datasets.
* The increase in accuracy from "ToT" to "Ours" is higher for "LogicNLI" (30.3%) compared to "ProofWriter" (25.7%).
* The "Ours" model achieves very high accuracy (close to 100%) on both datasets.
### Interpretation
The bar chart demonstrates that the "Ours" model has a substantially higher one-step inference accuracy compared to the "ToT" model on both the "ProofWriter" and "LogicNLI" datasets. The increase in accuracy is notable, suggesting that the "Ours" model is significantly better at performing one-step inference tasks on these datasets. The higher improvement on "LogicNLI" might indicate that the "Ours" model is particularly well-suited for this type of task. The near-perfect accuracy of the "Ours" model suggests it is highly effective for the evaluated tasks.
</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
## Chart: Search Error
### Overview
The image is a bar chart comparing the search error rates of different models (ToT, Ours) with and without search, across two datasets (ProofWriter, LogicNLI). The y-axis represents the error rate in percentage, and the x-axis represents the datasets. The chart includes a legend to distinguish between the different models and their search variants.
### Components/Axes
* **Title:** Search Error
* **Y-axis:** Error Rate (%)
* Scale: 0% to 40%
* **X-axis:** Datasets (ProofWriter, LogicNLI)
* **Legend:** Located at the bottom of the chart.
* ToT (light blue)
* ToT-Search (dark blue)
* Ours (light red)
* Ours-Search (dark red)
### Detailed Analysis
The chart presents error rates for four different configurations across two datasets.
**ProofWriter Dataset:**
* ToT: 31.0%
* ToT-Search: 14.0%
* Ours: 11.5%
* Ours-Search: 2.8%
**LogicNLI Dataset:**
* ToT: 43.2%
* ToT-Search: 16.0%
* Ours: 29.5%
* Ours-Search: 5.0%
### Key Observations
* For both datasets, the "Search" variants (ToT-Search and Ours-Search) consistently exhibit lower error rates compared to their non-search counterparts (ToT and Ours).
* The LogicNLI dataset generally shows higher error rates across all configurations compared to the ProofWriter dataset.
* "Ours-Search" achieves the lowest error rate in both datasets.
### Interpretation
The data suggests that incorporating a search mechanism significantly reduces the error rate for both the "ToT" and "Ours" models. The "Ours-Search" model appears to be the most effective, achieving the lowest error rates across both datasets. The higher error rates on the LogicNLI dataset might indicate that this dataset is more challenging for these models. The chart highlights the benefit of using search algorithms to improve the performance of these models in terms of reducing search errors.
</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
## Line Chart: Accuracy vs. Reasoning Depth
### Overview
The image is a line chart comparing the accuracy of four different methods (CoT, Logic-LM, SymbCoT, and "Ours") against varying reasoning depths. The chart displays how the accuracy of each method changes as the reasoning depth increases.
### Components/Axes
* **X-axis:** Reasoning Depth, with markers at 0, 1, 2, 3, and 5.
* **Y-axis:** Accuracy %, ranging from 50 to 100 with markers at 60, 70, 80, 90, and 100.
* **Legend:** Located in the center of the lower portion of the chart.
* CoT (blue line with square markers)
* Logic-LM (blue line with circle markers)
* SymbCoT (blue line with triangle markers)
* Ours (red line with diamond markers)
### Detailed Analysis
* **CoT (Blue Squares):** The accuracy of CoT decreases as reasoning depth increases.
* Reasoning Depth 0: Accuracy ~77%
* Reasoning Depth 1: Accuracy ~74%
* Reasoning Depth 2: Accuracy ~66%
* Reasoning Depth 3: Accuracy ~59%
* Reasoning Depth 5: Accuracy ~51%
* **Logic-LM (Blue Circles):** The accuracy of Logic-LM decreases slightly as reasoning depth increases.
* Reasoning Depth 0: Accuracy ~82%
* Reasoning Depth 1: Accuracy ~78%
* Reasoning Depth 2: Accuracy ~74%
* Reasoning Depth 3: Accuracy ~72%
* Reasoning Depth 5: Accuracy ~72%
* **SymbCoT (Blue Triangles):** The accuracy of SymbCoT decreases as reasoning depth increases.
* Reasoning Depth 0: Accuracy ~90%
* Reasoning Depth 1: Accuracy ~93%
* Reasoning Depth 2: Accuracy ~86%
* Reasoning Depth 3: Accuracy ~81%
* Reasoning Depth 5: Accuracy ~73%
* **Ours (Red Diamonds):** The accuracy of "Ours" decreases as reasoning depth increases.
* Reasoning Depth 0: Accuracy ~99%
* Reasoning Depth 1: Accuracy ~93%
* Reasoning Depth 2: Accuracy ~87%
* Reasoning Depth 3: Accuracy ~82%
* Reasoning Depth 5: Accuracy ~78%
### Key Observations
* "Ours" method starts with the highest accuracy at reasoning depth 0.
* All methods show a decrease in accuracy as reasoning depth increases.
* CoT experiences the most significant drop in accuracy with increasing reasoning depth.
* Logic-LM maintains a relatively stable accuracy across different reasoning depths.
### Interpretation
The chart illustrates the performance of different reasoning methods as the complexity of the reasoning task increases (indicated by reasoning depth). The "Ours" method initially outperforms the others but experiences a decline in accuracy with increasing reasoning depth, although it remains the highest performing method. CoT's performance degrades significantly with deeper reasoning, suggesting it may not be as robust for complex tasks. Logic-LM shows more consistent performance, indicating better stability across different reasoning depths. SymbCoT starts with a high accuracy but also declines as reasoning depth increases. The data suggests that the choice of reasoning method is crucial and depends on the complexity of the task at hand.
</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
## Pie Chart Comparison: ProofWriter vs. LogicNLI
### Overview
The image presents two pie charts side-by-side, comparing the distribution of different categories for "ProofWriter" and "LogicNLI". Each slice of the pie represents a percentage of the whole, with categories including Translation, Decompose, Resolve, Search, Imax, and Contra Error.
### Components/Axes
* **Titles:** "ProofWriter" (left pie chart), "LogicNLI" (right pie chart)
* **Categories:**
* Translation (peach color)
* Decompose (light green color)
* Resolve (light pink color)
* Search (light yellow color)
* Imax (light blue color)
* Contra Error (gray color)
* **Percentages:** Displayed directly on each slice of the pie charts.
* **Legend:** Located at the bottom of the image, mapping colors to categories.
### Detailed Analysis
**ProofWriter Pie Chart:**
* Contra Error (gray): 27.0%
* Imax (light blue): 18.9%
* Search (light yellow): 24.3%
* Resolve (light pink): 8.1%
* Decompose (light green): 10.8%
* Translation (peach): 10.8%
**LogicNLI Pie Chart:**
* Contra Error (gray): 33.3%
* Imax (light blue): 7.1%
* Search (light yellow): 16.7%
* Resolve (light pink): 9.5%
* Decompose (light green): 9.5%
* Translation (peach): 23.8%
### Key Observations
* **Contra Error:** The "Contra Error" category has the largest percentage in both pie charts, with LogicNLI having a significantly higher percentage (33.3%) compared to ProofWriter (27.0%).
* **Translation:** "Translation" has a higher percentage in LogicNLI (23.8%) compared to ProofWriter (10.8%).
* **Imax:** "Imax" has a significantly lower percentage in LogicNLI (7.1%) compared to ProofWriter (18.9%).
* **Search:** "Search" has a lower percentage in LogicNLI (16.7%) compared to ProofWriter (24.3%).
* **Decompose & Resolve:** The percentages for "Decompose" and "Resolve" are relatively similar between the two pie charts.
### Interpretation
The pie charts provide a comparative view of how different categories are distributed between "ProofWriter" and "LogicNLI". The most notable difference is in the "Contra Error" category, which is substantially larger in "LogicNLI," suggesting that "LogicNLI" may encounter more errors of this type or that this category is more prominent in its operation. Conversely, "Imax" is significantly smaller in "LogicNLI," indicating that this aspect plays a lesser role compared to "ProofWriter." The variations in "Translation" and "Search" also highlight differences in the processes or tasks performed by each system. The similarity in "Decompose" and "Resolve" suggests that these aspects are relatively consistent between the two.
</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 ( $→$ ) 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}← T(P,S)$ ;
// Translate the given premises and statement
$P_{n},S_{n}← D(P_{t},S_{t})$ ;
// Decompose the translated premises and statement
$C_{\text{current\_list}}←[S_{n},\neg S_{n}]$ ;
// Initiate search with $S_{n}$ and its negation
1 $Search\_round← 0$ ;
2
3 foreach $C_{\text{current}}$ in $C_{\text{current\_list}}$ do
4 while $Search\_round<S$ do
$C_{\text{searched\_list}}← SR(C_{\text{current}},P_{n})$ ;
// Search for complementary clause
5 $num\_searched\_C←\text{len}(C_{\text{searched\_list}})$ ;
6
7 if $num\_searched\_C>=1$ then
8 $C_{\text{searched}}← C_{\text{searched\_list}}[0]$ ;
9
10 else
11 $C_{\text{searched}}← C_{\text{searched\_list}}.\text{pop}(0)$ ;
12
13 end if
14
$cache←\{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}}←\text{next}(\text{iter}(\text{cache}))$ ;
// If no $C_{c}urrent$ found, search from $cache$
18 $C_{\text{searched}}←\text{cache}[C_{\text{current}}].\text{pop}(0)$ ;
19
20 end if
21 else
22 if Start from $S_{n}$ then
$D_{S_{n}}← 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}}← P\not\vdash S$ ;
27
28 end if
29 break;
30
31 end if
32
33 end if
34
35 $C_{\text{resolved}}← 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}}← 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}}← P\vdash S$ ;
42
43 end if
44 break;
45
46 end if
47 else
$P_{n}← P_{n}\cup\{C_{\text{resolved}}\}$ ;
// Append $C_{\text{resolved}}$ on $P_{n}$
48
49 end if
50 $C_{\text{current}}← C_{\text{resolved}}$ ;
51
52 end while
53 if Start from $S_{n}$ then
$D_{S_{n}}← 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}}← 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 ::: $∀ x\left(\text{Green}(x,\text{False})\lor\text{Nice}(x,\text{True})\right)$ 2.
If someone is smart then they are green ::: $∀ 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}}=∀ 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}}=∀ 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 ::: $∀ x\left(\text{Green}(x,\text{False})\lor\text{Nice}(x,\text{True})\right)$ 2.
If someone is smart then they are green ::: $∀ 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)→ Shy(x,False)$ •
$Jompus(x,True)→ 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…)