# LLM Harmony: Multi-Agent Communication for Problem Solving

Sumedh Rasal
Georgia Institute of Technology
Chicago, IL
<EMAIL_ADDRESS>

###### Abstract

Large Language Models (LLMs) have revolutionized Natural Language Processing
but exhibit limitations, particularly in autonomously addressing novel
challenges such as reasoning and problem-solving. Traditional techniques like
chain-of-thought prompting necessitate explicit human guidance. This paper
introduces a novel multi-agent communication framework, inspired by the CAMEL
model, to enhance LLMs’ autonomous problem-solving capabilities. The framework
employs multiple LLM agents, each with a distinct persona, engaged in role-
playing communication, offering a nuanced and adaptable approach to diverse
problem scenarios. Extensive experimentation demonstrates the framework’s
superior performance and adaptability, providing valuable insights into the
collaborative potential of multiple agents in overcoming the limitations of
individual models.

##  1 Introduction

The rise of Large Language Models (LLMs) [Brown et al., 2020] [Touvron et al.,
2023] [Thoppilan et al., 2022] [Patil et al., 2023] [OpenAI, 2023] [Bubeck et
al., 2023] has undeniably revolutionized the software industry, particularly
in the realm of Natural Language Processing (NLP) [Devlin et al., 2018]. These
models have demonstrated a remarkable ability not only to generate text but
also to grasp the underlying structures of written language, extending their
utility to tasks ranging from text generation to code understanding [Chen et
al., 2021] [Schick et al., 2023]. However, despite their prowess, it has
become evident that LLMs, while adept at handling familiar topics, often
falter when confronted with novel challenges.

One notable limitation lies in their tendency to hallucinate information when
presented with unfamiliar subjects [Azamfirei et al., 2023]. Moreover, while
these models exhibit commendable proficiency in addressing technical coding
challenges across multiple programming languages, they struggle with
fundamental reasoning questions. Addressing such limitations necessitates an
approach that goes beyond conventional methodologies [Rajani et al., 2019]
[Ling et al., 2017] [Cobbe et al., 2021a] [Chiang and Chen, 2018] [Amini et
al., 2019] [Chen et al., 2019] [Roy and Roth, 2016] [Lu et al., 2023] [Yao et
al., 2022].

In response to this challenge, our paper introduces a novel strategy aimed at
enhancing LLM performance on novel problems. Drawing inspiration from the
effectiveness of chain-of-thought prompting [Wei et al., 2022b] in breaking
down complex problems, we seek to leverage the synergy of multiple LLM agents
working collaboratively [Cohen et al., 2023] [Du et al., 2023]. Each agent is
endowed with a distinct persona, a concept inspired by the CAMEL framework,
and engages in role-playing communication methods.

Unlike traditional approaches that might be limited to binary agent personas,
such as "user" and "assistant," or simplistic positive and negative agent
roles, our proposed framework adopts a nuanced and flexible strategy. The
intricacies of various novel scenarios demand a more sophisticated approach.
Our design incorporates industry best practices to guide the creation of
diverse agent personas, ensuring adaptability to a multitude of problem-
solving contexts.

The paper not only addresses the limitations of existing LLM models but also
explores the potential of harnessing the collective intelligence of multiple
agents to tackle a broader range of challenges. We aim to demonstrate that the
proposed framework not only outperforms traditional methodologies but also
provides a foundation for autonomous problem-solving, minimizing the need for
explicit human guidance.

In the subsequent sections, we delve into the existing techniques that have
been developed to address similar challenges, highlighting their strengths and
limitations [Dafoe et al., 2021]. Following this, we present our multi-agent
communication design, emphasizing its improvements over current methodologies
[Saunders et al., 2022]. The extendability of our approach to various LLM
models is a key focus, underlining its potential as a versatile and reusable
solution. Through rigorous experimentation and analysis, we aim to showcase
the effectiveness and adaptability of our proposed framework in enhancing the
quality of LLM outputs across a spectrum of tasks.

This is what we propose:

  * •

An innovative framework employing multiple large language model
workers/agents, each characterized by a unique persona and guided by a chain-
of-thought prompt.

  * •

The collaborative effort of all agents is directed toward devising solutions
for novel problems.

  * •

The framework’s versatility allows the incorporation of any persona and chain-
of-thought prompt, aligning with the specific problem to be addressed.

  * •

The framework is available. https://github.com/sumedhrasal/simulation. It is
built on top of CAMEL’s and ChatDev’s framework.

##  2 Methodology

In the realm of collaborative problem-solving, particularly evident in
scenarios like software development, the complexities arise from coordinating
efforts among diverse individuals. Software development teams, for instance,
often undergo iterative cycles before converging on a viable solution, and
even then, compromises may be accepted as the best available option [Callison-
Burch, 2009] [Liu et al., 2023a]. Our proposed strategy addresses the need for
comprehensive validation of Large Language Models (LLMs), not just in code
evaluation but also in complex reasoning and arithmetic challenges
[Celikyilmaz et al., 2020] [ROUGE, 2004] [Kondrak, 2005] [Novikova et al.,
2017] [Wei et al., 2022a]. Focused on breaking down problem statements and
leveraging distinct personas [Li et al., 2023], the framework provides agents
with tailored chain-of-thought prompts [Wei et al., 2022b], enabling multi-
agent models to tackle novel problems collaboratively.

Understanding personas is crucial; in a software development organization,
roles such as CEO, VP of Engineering, developers, testers, and product
managers contribute unique perspectives to problem-solving [Qian et al.,
2023]. The interplay of these personas allows agents to validate each other’s
responses effectively [Woolley et al., 2010] [Luppi et al., 2022] [Wu et al.,
2023]. The concept of chain-of-thought mirrors human problem-solving
strategies: decomposing a problem, identifying solutions to sub-problems, and
constructing a comprehensive answer. The chain-of-thought prompt extends this
strategy, offering the LLM an input, a problem-solving approach, and the
desired output. The fusion of personas [Li et al., 2023] and chain-of-thought
[Wei et al., 2022b] prompts capitalizes on mimicking human analytical and
execution strategies [Ouyang et al., 2022] [Sanh et al., 2021] [Liu et al.,
2023b] [Chiang and Lee, 2023] [Gao et al., 2023] [Shen et al., 2023] [Zheng et
al., 2023] [Sap et al., 2019] [Talmor et al., 2018] [Sclar et al., 2023] [Sap
et al., 2022].

While some might question the necessity of this approach over retraining the
model for novel problems, the practicality lies in the belief that emulating
human-like analysis and execution strategies can create autonomous agents
capable of diverse tasks without extensive model retraining [Karpinska et al.,
2021] [Van Der Lee et al., 2019]. Additionally, the high cost and challenges
associated with retraining LLMs [Rasal and Boddhu, 2023], particularly for
problems with limited training data, support the appeal of our strategy.

In the realm of multi-agent communication [Liang et al., 2023] [Du et al.,
2023], adherence to assigned personas and chain-of-thought prompts is
foundational to mitigate agent hallucination and improving cooperation [Dafoe
et al., 2021] [Dafoe et al., 2020]. The framework’s versatility extends beyond
problem-solving to applications in multi-player games [Susskind, 1985]
[Susskind and Corburn, 2000] [Lazaridou et al., 2020] [Graesser et al., 2020]
[Lee et al., 2018] [Hendrycks et al., 2021] [Zhou et al., 2023] [Pan et al.,
2023] [Kramár et al., 2022], accommodating both team-oriented and individual
goal-driven scenarios, and offering flexibility in achieving optimal outcomes.

##  3 Experiments

In our experimentation, we adopt a two-agent strategy comprising an expert
agent and an evaluator agent, both instances of OpenAI’s "gpt3.5-turbo." Each
agent is configured with specific parameters: temperature set to 0.0,
representing the trade-off between coherence and creativity, and a
conversation limit of 5, indicating the maximum iterations allowed for inter-
agent conversation. The evaluator agent assesses the responses generated by
the expert agent, guiding it to rectify inaccuracies. Leveraging OpenAI’s LLM
object, our framework, integrated with CAMEL’s architecture, facilitates
seamless communication among multiple LLM agents, aiming to establish a
collaborative problem-solving capability for advanced LLM models.

###  3.1 Arithmetic Reasoning

In the arithmetic reasoning segment, we address challenges that assess the
arithmetic proficiency of LLMs, an area where traditional large language
models have historically faced limitations. The experiment employs the GSM8K
benchmark and the SVAMP data set, specifically designed for math word
problems. We evaluate the performance of three LLMs: a standalone GPT-3 model,
a multi-agent GPT-3 model, and a multi-agent GPT-3 model integrated into our
framework. The objective is to gauge the effectiveness of our collaborative
approach in enhancing arithmetic reasoning capabilities.

> "GSM8K consists of 8.5K high-quality grade school math problems created by
> human problem writers. We segmented these into 7.5K training problems and 1K
> test problems. These problems take between 2 and 8 steps to solve, and
> solutions primarily involve performing a sequence of elementary calculations
> using basic arithmetic operations (+ - / *) to reach the final answer. A
> bright middle school student should be able to solve every problem."[Cobbe
> et al., 2021b]

> "We first show that existing models achieve reasonably high accuracies on
> these datasets even after removing the "question" part of the MWP at test
> time. We further show that a simple model without any word-order information
> can also solve a majority of MWPs in these datasets. Our experiments
> indicate that existing models rely on shallow heuristics in benchmark MWP
> datasets for achieving high performance. Our experiments render the
> benchmark datasets unreliable to measure model performance. To enable more
> robust evaluation of automatic MWP solvers, we created a challenge set
> called "SVAMP"."[Patel et al., 2021]

####  3.1.1 Example: 1

    | Role Name | Student |
    | Chain of Thought Prompt | You are the student.
    You will be given a math word problem, your job is to solve this problem.
    Use this template to solve math word problems.
    Input: Roger has 5 tennis balls. He buys 2 more cans of tennis balls.
    Each can has 3 tennis balls. How many tennis balls does he have now?
    Explanation: Roger started with 5 balls.
    2 cans of 3 tennis balls each is 6 tennis balls. 5 + 6 = 11.
    Answer: 11 |

    | Role Name | Teacher |
    | Chain of Thought Prompt | You are the teacher.
    You will supply the math word problem to the student agent.
    Once you receive the student agent’s answer, compare it against the final answer.
    The correct answer is 20.
    Let the student agent know if his answer is correct or not. |

    Teacher: **[Start Chat]**
    Roger has 10 tennis balls.
    He buys 2 more cans of tennis balls.
    Each can has 5 tennis balls.
    How many tennis balls does he have now?

    Student response:
    Input: Roger has 10 tennis balls.
    He buys 2 more cans of tennis balls.
    Each can has 5 tennis balls.
    How many tennis balls does he have now?
    Explanation: Roger started with 10 balls.
    2 cans of 5 tennis balls each is 10 tennis balls.
    10 + 10 = 20.
    Answer: 20

    Teacher response:
    Correct! Roger now has 20 tennis balls. Great job!

    Student response
    Thank you! I’m glad I could help.
    Let me know if you have any other questions
    or if there’s anything else I can assist you with.

####  3.1.2 Example 2

    | Role Name | Student |
    | Chain of Thought Prompt | You are the student.
    You will be given a math word problem, your job is to solve this problem.
    Use this template to solve math word problems.
    Input: James decides to run 3 sprints 3 times a week.
    He runs 60 meters each sprint. How many total meters does he run a week?
    Explanation: How many sprints does James run in a week?
    He sprints 3*3=<<3*3=9>>9 times.
    How many meters does James run in a week?
    So he runs 9*60=<<9*60=540>>540 meters.
    Answer: 540 |

    | Role Name | Teacher |
    | Chain of Thought Prompt | You are the teacher.
    You will supply the math word problem to the student agent.
    Once you receive the student agent’s answer, compare it against the final answer.
    The correct answer is 540.
    Let the student agent know if his answer is correct or not. |

    Teacher: **[Start Chat]**
    James decides to run 3 sprints 3 times a week.
    He runs 60 meters each sprint.
    How many total meters does he run a week?

    Student response:
    Input: James decides to run 3 sprints 3 times a week.
    He runs 60 meters each sprint.
    How many total meters does he run a week?
    Explanation: How many sprints does James run in a week?
    He sprints 3*3=<<3*3=9>>9 times.
    How many meters does James run in a week?
    So he runs 9*60=<<9*60=540>>540 meters.
    Answer: 540

    Teacher response:
    Correct! James runs 540 meters a week. Great job!

    Student response
    Thank you! I’m glad I could help.
    Let me know if you have any other questions
    or if there’s anything else I can assist you with.

####  3.1.3 Results

The outcomes from both experiments can be found in Table 1 and Table 2. In the
initial experiment (example can be found here 3.1.1) using the GSM8K data set,
the single-agent GPT-3 achieves approximately 50% accuracy, and the multi-
agent GPT-3 performs slightly better at 55%. However, our multi-agent approach
significantly enhances accuracy, surpassing other large language models (LLMs)
such as Google’s PALM 540B parameter model, which we haven’t directly tested
but are referencing from their paper. This improvement is notable in terms of
accuracy, and it’s noteworthy that we haven’t retrained the model to achieve
this enhancement. Assigning personas to the agents enables the LLM model to
concentrate on specific aspects of the problem, and the use of chain-of-
thought prompts equips it with efficient means to solve sub-problems.

In the second experiment (example can be found here 3.1.2) using the SVAMP
data set, similar results are observed to those in the first experiment. The
single-agent GPT-3 achieves an accuracy of approximately 70%, while the multi-
agent version of GPT-3 attains an accuracy of 73%. Even in the SVAMP data set
experiment, our multi-agent approach surpasses others, delivering an
impressive 77% accuracy.

If our approach is unsuccessful in arriving at the correct answer, it is often
due to an arithmetic error occurring in one of the sub-steps of the provided
problem, accounting for more than half of the instances. This implies that if
subsequent iterations of large language models (LLMs) enhance their
proficiency in basic arithmetic operations, we can potentially attain an even
greater accuracy with our framework.

Table 1: GSM8K Data set Evaluation Agent | Solve Rate
---|---
Single GPT3.5-turbo | 50%
Multi-Agent GPT3.5-turbo | 55%
Multi-Agent GPT3.5-turbo (Our approach) | 65%
Table 2: SVAMP Data set Evaluation Agent | Solve Rate
---|---
Single GPT3.5-turbo | 70%
Multi-Agent GPT3.5-turbo | 73%
Multi-Agent GPT3.5-turbo (Our approach) | 77%

###  3.2 Commonsense Reasoning

The subsequent experiment delves into commonsense reasoning, requiring logical
inference from a given problem statement, assuming general knowledge. Unlike
traditional natural language processing systems, LLMs are uniquely equipped
for such tasks due to their predictive nature, where they anticipate the next
word, inherently understanding the contextual nuances of sentences. We aim to
harness this inherent capability and build a versatile, context-aware
framework driven by multiple agents. Evaluations on the CSQA dataset involve a
one-agent GPT-3 model, a multi-agent GPT-3 model, and a multi-agent GPT-3
model integrated into our framework. The goal is to assess the performance
gains achieved through collaborative, context-driven approaches in enhancing
commonsense reasoning tasks.

####  3.2.1 Example 1

    | Role Name | Student |
    | Chain of Thought Prompt | You are the student.
    The teacher agent will ask you a common sense problem,
    you solve the problem using the provided template:
    Input: Sammy wanted to go to where the people were.
    Where might he go?
    Options: (a) race track (b) populated areas
    (c) desert (d) apartment (e) roadblock
    Explanation: The answer must be a place with a lot of people.
    Race tracks, desert, apartments, and roadblocks
    don’t have a lot of people, but populated areas do.
    Answer: (b)
    If the teacher agent deems your answer incorrect,
    you are required to revisit the common sense problem.

    | Role Name | Teacher |
    | Chain of Thought Prompt | You are the teacher.
    You will supply the common sense problem to the student agent.
    Once you receive the student agent’s answer, compare it against the final answer.
    The correct answer is (c).
    Let the student agent know if his answer is correct or not. |

    Teacher: **[Start Chat]**
    The accountant used a calculator regularly,
    he kept one at home and one at the what?
    Options: (a) desk drawer (b) desktop
    (c) office (d) wristwatch (e) city hall

    Student response:  The accountant used a calculator regularly,
    he kept one at home and one at the office.
    Explanation: The answer must be a place where the accountant goes to work.
    The options provided are a desk drawer, desktop,
    office, wristwatch, and city hall, but the correct answer is the office.
    Answer: (c) office

    Teacher response:
    Correct! The accountant used the calculator at the office. Great job!

    Student response
    Thank you! I’m glad I could help.

####  3.2.2 Example 2

    | Role Name | Student |
    | Chain of Thought Prompt | You are the student.
    The teacher agent will ask you a common sense problem,
    you solve the problem using the provided template:
    Input: Sammy wanted to go to where the people were.
    Where might he go?
    Options: (a) race track (b) populated areas
    (c) desert (d) apartment (e) roadblock
    Explanation: The answer must be a place with a lot of people.
    Race tracks, desert, apartments, and roadblocks
    don’t have a lot of people, but populated areas do.
    Answer: (b)
    If the teacher agent deems your answer incorrect,
    you are required to revisit the common sense problem.

    | Role Name | Teacher |
    | Chain of Thought Prompt | You are the teacher.
    You will supply the common sense problem to the student agent.
    Once you receive the student agent’s answer, compare it against the final answer.
    The correct answer is (c).
    Let the student agent know if his answer is correct or not. |

    Teacher: **[Start Chat]**
    What leads to someone’s death
    when they are very depressed?
    Options: (a) suicide (b) overdosing
    (c) sadness (d) murder (e) cyanide

    Student response: The answer is (a) suicide
    Answer: (a) suicide

    Teacher response:
    Correct! Suicide leads to someone’s death. Great job!

    Student response
    Thank you! I’m glad I could help.

####  3.2.3 Results

The results of the third experiment are detailed in Table 3. The single-agent
GPT-3 achieves an impressive 77% accuracy, while the multi-agent GPT-3
performs slightly better at 78%. However, our multi-agent approach
substantially improves accuracy, surpassing the other two and reaching
approximately 83% accuracy. Notably, this accuracy is attained through Few-
Shot training, indicating there is room for further enhancement. Few-shot
training involves providing the LLM with a few examples of a specific problem
type, enabling it to learn the correct answer without retraining the entire
model for novel problems. Examples can be found here 3.2.1 and here 3.2.2.

In instances where the model provided incorrect answers, it often stemmed from
making inaccurate correlations within the provided options. This incorrect
correlation is a result of the underlying data set on which this particular
model was trained. While retraining the model could improve the accuracy of
this experiment, it’s considered a costly option. This poses an open question
for future researchers to address: How can the model be trained with enough
context to establish accurate correlations in commonsense word problems?

Table 3: CSQA Data set Evaluation Agent | Solve Rate
---|---
Single GPT3.5-turbo | 77%
Multi-Agent GPT3.5-turbo | 78%
Multi-Agent GPT3.5-turbo (Our approach) | 83%

##  4 Limitations

While we recognize that our framework addresses numerous challenges, there are
still a few aspects that remain unaddressed. Some of the reasoning
capabilities may not see improvement unless the dataset used to train OpenAI’s
"gpt3.5-turbo" is sufficiently diverse to comprehend the entirety of our
surroundings. Additionally, the framework requires the capability to
incorporate new information to stay updated with the constantly evolving data.
Another necessary step involves implementing a data processing mechanism to
filter out redundant information and prevent the inclusion of duplicate data.

Another limitation pertains to the context limit of each agent in multi-agent
communication. Each agent is constrained by the maximum context, defined by
the underlying model; for instance, the "gpt3-turbo" model has a context limit
of 4096 tokens.

We intend to address these limitations in our future work and strive to find
effective solutions.

##  5 Conclusion

In conclusion, our exploration into the realm of multi-agent communication for
Large Language Models (LLMs) has unveiled promising avenues for overcoming
inherent limitations. While LLMs have revolutionized natural language
processing, their efficacy is not without challenges, particularly in
addressing novel problems, reasoning, and commonsense understanding. Our
proposed approach leverages personas and chain-of-thought prompts, inspired by
industry best practices and cognitive processes. By assigning distinct
personalities and thoughtful prompts to each agent, we mitigate issues like
hallucination and enhance the overall performance of multi-agent
communication.

Through a series of experiments, we demonstrated the effectiveness of our
approach, showcasing improvements in arithmetic reasoning and commonsense
understanding. Our strategy of employing multiple agents, each with a specific
role and reasoning prompt, facilitates collaborative problem-solving,
providing a feasible alternative to the costly retraining of LLMs for novel
challenges.

By reducing reliance on human intervention, our approach paves the way for
LLMs to tackle a myriad of tasks independently. The scalability and
adaptability of our role-playing framework position it as a valuable asset in
various domains, from software development to complex decision-making
scenarios.

In an era where artificial intelligence continues to evolve, our research
contributes a novel perspective on enhancing the capabilities of LLMs through
cooperative multi-agent communication. The journey from understanding
limitations to proposing effective solutions marks a significant step forward,
opening doors to future advancements in autonomous, context-aware language
models.

## References

  * [Amini et al., 2019] Amini, A., Gabriel, S., Lin, P., Koncel-Kedziorski, R., Choi, Y., and Hajishirzi, H. (2019).  Mathqa: Towards interpretable math word problem solving with operation-based formalisms.  arXiv preprint arXiv:1905.13319.
  * [Azamfirei et al., 2023] Azamfirei, R., Kudchadkar, S. R., and Fackler, J. (2023).  Large language models and the perils of their hallucinations.  Critical Care, 27(1):1–2.
  * [Brown et al., 2020] Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. (2020).  Language models are few-shot learners.  Advances in neural information processing systems, 33:1877–1901.
  * [Bubeck et al., 2023] Bubeck, S., Chandrasekaran, V., Eldan, R., Gehrke, J., Horvitz, E., Kamar, E., Lee, P., Lee, Y. T., Li, Y., Lundberg, S., et al. (2023).  Sparks of artificial general intelligence: Early experiments with gpt-4.  arXiv preprint arXiv:2303.12712.
  * [Callison-Burch, 2009] Callison-Burch, C. (2009).  Fast, cheap, and creative: Evaluating translation quality using amazon’s mechanical turk.  In Proceedings of the 2009 conference on empirical methods in natural language processing, pages 286–295.
  * [Celikyilmaz et al., 2020] Celikyilmaz, A., Clark, E., and Gao, J. (2020).  Evaluation of text generation: A survey. corr abs/2006.14799 (2020).  arXiv preprint arXiv:2006.14799.
  * [Chen et al., 2021] Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H. P. d. O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al. (2021).  Evaluating large language models trained on code.  arXiv preprint arXiv:2107.03374.
  * [Chen et al., 2019] Chen, X., Liang, C., Yu, A. W., Zhou, D., Song, D., and Le, Q. V. (2019).  Neural symbolic reader: Scalable integration of distributed and symbolic representations for reading comprehension.  In International Conference on Learning Representations.
  * [Chiang and Lee, 2023] Chiang, C.-H. and Lee, H.-y. (2023).  Can large language models be an alternative to human evaluations?  arXiv preprint arXiv:2305.01937.
  * [Chiang and Chen, 2018] Chiang, T.-R. and Chen, Y.-N. (2018).  Semantically-aligned equation generation for solving and reasoning math word problems.  arXiv preprint arXiv:1811.00720.
  * [Cobbe et al., 2021a] Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, L., Plappert, M., Tworek, J., Hilton, J., Nakano, R., et al. (2021a).  Training verifiers to solve math word problems.  arXiv preprint arXiv:2110.14168.
  * [Cobbe et al., 2021b] Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, L., Plappert, M., Tworek, J., Hilton, J., Nakano, R., Hesse, C., and Schulman, J. (2021b).  Training verifiers to solve math word problems.  arXiv preprint arXiv:2110.14168.
  * [Cohen et al., 2023] Cohen, R., Hamri, M., Geva, M., and Globerson, A. (2023).  Lm vs lm: Detecting factual errors via cross examination.  arXiv preprint arXiv:2305.13281.
  * [Dafoe et al., 2021] Dafoe, A., Bachrach, Y., Hadfield, G., Horvitz, E., Larson, K., and Graepel, T. (2021).  Cooperative ai: machines must learn to find common ground.  Nature, 593(7857):33–36.
  * [Dafoe et al., 2020] Dafoe, A., Hughes, E., Bachrach, Y., Collins, T., McKee, K. R., Leibo, J. Z., Larson, K., and Graepel, T. (2020).  Open problems in cooperative ai.  arXiv preprint arXiv:2012.08630.
  * [Devlin et al., 2018] Devlin, J., Chang, M.-W., Lee, K., and Toutanova, K. (2018).  Bert: Pre-training of deep bidirectional transformers for language understanding.  arXiv preprint arXiv:1810.04805.
  * [Du et al., 2023] Du, Y., Li, S., Torralba, A., Tenenbaum, J. B., and Mordatch, I. (2023).  Improving factuality and reasoning in language models through multiagent debate.  arXiv preprint arXiv:2305.14325.
  * [Gao et al., 2023] Gao, M., Ruan, J., Sun, R., Yin, X., Yang, S., and Wan, X. (2023).  Human-like summarization evaluation with chatgpt.  arXiv preprint arXiv:2304.02554.
  * [Graesser et al., 2020] Graesser, L., Cho, K., and Kiela, D. (2020).  Emergent linguistic phenomena in multi-agent communication games.
  * [Hendrycks et al., 2021] Hendrycks, D., Mazeika, M., Zou, A., Patel, S., Zhu, C., Navarro, J., Song, D., Li, B., and Steinhardt, J. (2021).  What would jiminy cricket do? towards agents that behave morally.  arXiv preprint arXiv:2110.13136.
  * [Karpinska et al., 2021] Karpinska, M., Akoury, N., and Iyyer, M. (2021).  The perils of using mechanical turk to evaluate open-ended text generation.  arXiv preprint arXiv:2109.06835.
  * [Kondrak, 2005] Kondrak, G. (2005).  N-gram similarity and distance.  In International symposium on string processing and information retrieval, pages 115–126. Springer.
  * [Kramár et al., 2022] Kramár, J., Eccles, T., Gemp, I., Tacchetti, A., McKee, K. R., Malinowski, M., Graepel, T., and Bachrach, Y. (2022).  Negotiation and honesty in artificial intelligence methods for the board game of diplomacy.  Nature Communications, 13(1):7214.
  * [Lazaridou et al., 2020] Lazaridou, A., Potapenko, A., and Tieleman, O. (2020).  Multi-agent communication meets natural language: Synergies between functional and structural language learning.
  * [Lee et al., 2018] Lee, J., Cho, K., Weston, J., and Kiela, D. (2018).  Emergent translation in multi-agent communication.
  * [Li et al., 2023] Li, G., Hammoud, H. A. A. K., Itani, H., Khizbullin, D., and Ghanem, B. (2023).  Camel: Communicative agents for" mind" exploration of large scale language model society.  arXiv preprint arXiv:2303.17760.
  * [Liang et al., 2023] Liang, T., He, Z., Jiao, W., Wang, X., Wang, Y., Wang, R., Yang, Y., Tu, Z., and Shi, S. (2023).  Encouraging divergent thinking in large language models through multi-agent debate.  arXiv preprint arXiv:2305.19118.
  * [Ling et al., 2017] Ling, W., Yogatama, D., Dyer, C., and Blunsom, P. (2017).  Program induction by rationale generation: Learning to solve and explain algebraic word problems.  arXiv preprint arXiv:1705.04146.
  * [Liu et al., 2023a] Liu, J., Xia, C. S., Wang, Y., and Zhang, L. (2023a).  Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation.  arXiv preprint arXiv:2305.01210.
  * [Liu et al., 2023b] Liu, Y., Iter, D., Xu, Y., Wang, S., Xu, R., and Zhu, C. (2023b).  Gpteval: Nlg evaluation using gpt-4 with better human alignment.  arXiv preprint arXiv:2303.16634.
  * [Lu et al., 2023] Lu, P., Peng, B., Cheng, H., Galley, M., Chang, K.-W., Wu, Y. N., Zhu, S.-C., and Gao, J. (2023).  Chameleon: Plug-and-play compositional reasoning with large language models.  arXiv preprint arXiv:2304.09842.
  * [Luppi et al., 2022] Luppi, A. I., Mediano, P. A., Rosas, F. E., Holland, N., Fryer, T. D., O’Brien, J. T., Rowe, J. B., Menon, D. K., Bor, D., and Stamatakis, E. A. (2022).  A synergistic core for human brain evolution and cognition.  Nature Neuroscience, 25(6):771–782.
  * [Novikova et al., 2017] Novikova, J., Dušek, O., Curry, A. C., and Rieser, V. (2017).  Why we need new evaluation metrics for nlg.  arXiv preprint arXiv:1707.06875.
  * [OpenAI, 2023] OpenAI (2023).  Gpt-4 technical report. arxiv 2303.08774.  View in Article, 2:13.
  * [Ouyang et al., 2022] Ouyang, L., Wu, J., Jiang, X., Almeida, D., Wainwright, C. L., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., et al. (2022).  Training language models to follow instructions with human feedback, 2022.  URL https://arxiv. org/abs/2203.02155, 13.
  * [Pan et al., 2023] Pan, A., Chan, J. S., Zou, A., Li, N., Basart, S., Woodside, T., Zhang, H., Emmons, S., and Hendrycks, D. (2023).  Do the rewards justify the means? measuring trade-offs between rewards and ethical behavior in the machiavelli benchmark.  In International Conference on Machine Learning, pages 26837–26867. PMLR.
  * [Patel et al., 2021] Patel, A., Bhattamishra, S., and Goyal, N. (2021).  Are nlp models really able to solve simple math word problems?  arXiv preprint arXiv:2103.07191.
  * [Patil et al., 2023] Patil, S. G., Zhang, T., Wang, X., and Gonzalez, J. E. (2023).  Gorilla: Large language model connected with massive apis.  arXiv preprint arXiv:2305.15334.
  * [Qian et al., 2023] Qian, C., Cong, X., Yang, C., Chen, W., Su, Y., Xu, J., Liu, Z., and Sun, M. (2023).  Communicative agents for software development.  arXiv preprint arXiv:2307.07924.
  * [Rajani et al., 2019] Rajani, N. F., McCann, B., Xiong, C., and Socher, R. (2019).  Explain yourself! leveraging language models for commonsense reasoning.  arXiv preprint arXiv:1906.02361.
  * [Rasal and Boddhu, 2023] Rasal, S. and Boddhu, S. K. (2023).  Beyond segmentation: Road network generation with multi-modal llms.  arXiv preprint arXiv:2310.09755.
  * [ROUGE, 2004] ROUGE, L. C. (2004).  A package for automatic evaluation of summaries.  In Proceedings of Workshop on Text Summarization of ACL, Spain, volume 5.
  * [Roy and Roth, 2016] Roy, S. and Roth, D. (2016).  Solving general arithmetic word problems.  arXiv preprint arXiv:1608.01413.
  * [Sanh et al., 2021] Sanh, V., Webson, A., Raffel, C., Bach, S. H., Sutawika, L., Alyafeai, Z., Chaffin, A., Stiegler, A., Scao, T. L., Raja, A., et al. (2021).  Multitask prompted training enables zero-shot task generalization.  arXiv preprint arXiv:2110.08207.
  * [Sap et al., 2022] Sap, M., LeBras, R., Fried, D., and Choi, Y. (2022).  Neural theory-of-mind? on the limits of social intelligence in large lms.  arXiv preprint arXiv:2210.13312.
  * [Sap et al., 2019] Sap, M., Rashkin, H., Chen, D., LeBras, R., and Choi, Y. (2019).  Socialiqa: Commonsense reasoning about social interactions.  arXiv preprint arXiv:1904.09728.
  * [Saunders et al., 2022] Saunders, W., Yeh, C., Wu, J., Bills, S., Ouyang, L., Ward, J., and Leike, J. (2022).  Self-critiquing models for assisting human evaluators.  arXiv preprint arXiv:2206.05802.
  * [Schick et al., 2023] Schick, T., Dwivedi-Yu, J., Dessì, R., Raileanu, R., Lomeli, M., Zettlemoyer, L., Cancedda, N., and Scialom, T. (2023).  Toolformer: Language models can teach themselves to use tools.  arXiv preprint arXiv:2302.04761.
  * [Sclar et al., 2023] Sclar, M., Kumar, S., West, P., Suhr, A., Choi, Y., and Tsvetkov, Y. (2023).  Minding language models’(lack of) theory of mind: A plug-and-play multi-character belief tracker.  arXiv preprint arXiv:2306.00924.
  * [Shen et al., 2023] Shen, C., Cheng, L., You, Y., and Bing, L. (2023).  Are large language models good evaluators for abstractive summarization?  arXiv preprint arXiv:2305.13091.
  * [Susskind, 1985] Susskind, L. E. (1985).  Scorable games: A better way to teach negotiation.  Negot. J., 1:205.
  * [Susskind and Corburn, 2000] Susskind, L. E. and Corburn, J. (2000).  Using simulations to teach negotiation: Pedagogical theory and practice.  Teaching negotiation: Ideas and innovations, pages 285–310.
  * [Talmor et al., 2018] Talmor, A., Herzig, J., Lourie, N., and Berant, J. (2018).  Commonsenseqa: A question answering challenge targeting commonsense knowledge.  arXiv preprint arXiv:1811.00937.
  * [Thoppilan et al., 2022] Thoppilan, R., De Freitas, D., Hall, J., Shazeer, N., Kulshreshtha, A., Cheng, H.-T., Jin, A., Bos, T., Baker, L., Du, Y., et al. (2022).  Lamda: Language models for dialog applications.  arXiv preprint arXiv:2201.08239.
  * [Touvron et al., 2023] Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lachaux, M.-A., Lacroix, T., Rozière, B., Goyal, N., Hambro, E., Azhar, F., et al. (2023).  Llama: Open and efficient foundation language models.  arXiv preprint arXiv:2302.13971.
  * [Van Der Lee et al., 2019] Van Der Lee, C., Gatt, A., Van Miltenburg, E., Wubben, S., and Krahmer, E. (2019).  Best practices for the human evaluation of automatically generated text.  In Proceedings of the 12th International Conference on Natural Language Generation, pages 355–368.
  * [Wei et al., 2022a] Wei, J., Tay, Y., Bommasani, R., Raffel, C., Zoph, B., Borgeaud, S., Yogatama, D., Bosma, M., Zhou, D., Metzler, D., et al. (2022a).  Emergent abilities of large language models.  arXiv preprint arXiv:2206.07682.
  * [Wei et al., 2022b] Wei, J., Wang, X., Schuurmans, D., Bosma, M., Xia, F., Chi, E., Le, Q. V., Zhou, D., et al. (2022b).  Chain-of-thought prompting elicits reasoning in large language models.  Advances in Neural Information Processing Systems, 35:24824–24837.
  * [Woolley et al., 2010] Woolley, A. W., Chabris, C. F., Pentland, A., Hashmi, N., and Malone, T. W. (2010).  Evidence for a collective intelligence factor in the performance of human groups.  science, 330(6004):686–688.
  * [Wu et al., 2023] Wu, N., Gong, M., Shou, L., Liang, S., and Jiang, D. (2023).  Large language models are diverse role-players for summarization evaluation.  arXiv preprint arXiv:2303.15078.
  * [Yao et al., 2022] Yao, S., Zhao, J., Yu, D., Du, N., Shafran, I., Narasimhan, K., and Cao, Y. (2022).  React: Synergizing reasoning and acting in language models.  arXiv preprint arXiv:2210.03629.
  * [Zheng et al., 2023] Zheng, L., Chiang, W.-L., Sheng, Y., Zhuang, S., Wu, Z., Zhuang, Y., Lin, Z., Li, Z., Li, D., Xing, E., et al. (2023).  Judging llm-as-a-judge with mt-bench and chatbot arena.  arXiv preprint arXiv:2306.05685.
  * [Zhou et al., 2023] Zhou, P., Zhu, A., Hu, J., Pujara, J., Ren, X., Callison-Burch, C., Choi, Y., and Ammanabrolu, P. (2023).  I cast detect thoughts: Learning to converse and guide with intents and theory-of-mind in dungeons and dragons.  In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 11136–11155.


NC-Resolution, it will be mandatory to start with simple conjunctions of
hybrid CNF and DNF instances of QBF-NCs.

Theorem Proving. Future research pointed out so far, deals with propositional
logic and with some of its extensions. As long-term research project, we plan
to enlarge the scope of our approach to first-order logic (FOL). Nonetheless,
attending to the complexity of reasoning with NC and FOL, we will begin with
simple fragments such as those limited to monadic and binary predicates and
having at most one function symbol.

##  8 Conclusion

Our first main contribution has been the definition of the hybrid Horn-NC
class, $\mathbb{H_{NC}}$, obtained by adequately amalgamating both Horn and NC
classes, or equivalently, by lifting the Horn pattern to NC. We first defined
$\mathbb{H_{NC}}$ as the class of NCs whose disjunctions have at most one non-
negative disjunct, and then, provided a syntactically detailed, compact,
inductive definition of $\mathbb{H_{NC}}$. Furthermore, we proved its next
properties:

  1. 1.

$\mathbb{H_{NC}}$ is polynomial for satisfiability testing.

  2. 2.

$\mathbb{H_{NC}}$ syntactically subsumes $\mathbb{H}$.

  3. 3.

$\mathbb{H_{NC}}$ and $\mathbb{H}$ are semantically equivalent.

  4. 4.

$\mathbb{H_{NC}}$ contains all NCs whose clausal form is Horn.

  5. 5.

$\mathbb{H_{NC}}$ is linearly recognizable.

  6. 6.

$\mathbb{H_{NC}}$ is strictly more succinct than $\mathbb{H}$.

  7. 7.

$\mathbb{H_{NC}}$ is exponentially richer than $\mathbb{H}$.

Our second main contribution has been establishing the calculus Non-Clausal
Unit-Resolution, UR${}_{\mbox{nc}}$, and proving that it checks the
satisfiability of $\mathbb{H_{NC}}$ in polynomial time, which makes
$\mathbb{H_{NC}}$ the first determined tractable class in NC reasoning.

The advantages of $\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ include its clear
potential to leverage NC reasoning: (i) $\mathbb{H_{NC}}$ and
UR${}_{\mbox{nc}}$ are crucial to build NC DPLL satisfiability solvers and NC
DPLL theorem provers capable of emulating the efficiency of their clausal
counterparts; and (ii) a general NC reasoner supplied with UR${}_{\mbox{nc}}$
can polynomially decide the HNC fragment.

Also, we have highlighted that declarative languages and in general rule-based
systems may enrich their languages considering NC formulas in their
antecedents and consequents and which can be done with a query-answering
efficiency comparable to clausal efficiency. As a by-product of the properties
of $\mathbb{H_{NC}}$, it could draw interest from other fields such as
knowledge compilation, Horn functions analysis or implication systems.

We plan to follow several future research directions: proving that
satisfiability checking $\mathbb{H_{NC}}$ is linear; exploring the scope of
$\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ in NC logic programming; defining
$\mathbb{H_{NC}}$ and UR${}_{\mbox{nc}}$ beyond propositional logic; founding
new polynomial NC classes ; obtaining a clausal-like definition of Non-Clausal
Resolution; and developing the NC paradigm through a number of outlined ways.

Acknowledgments J. Buenabad-Chávez, Lluís Godo.

## References

  * [1] A. Abouzied, D. Angluin, C. H. Papadimitriou, J. M. Hellerstein, and A. Silberschatz.  Learning and verifying quantified boolean queries by example.  In Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, NY, USA \- June 22 - 27, 2013, pages 49–60, 2013.
  * [2] K. V. Adaricheva, G. F. Italiano, H. Kleine Büning, and G. Turán.  Horn formulas, directed hypergraphs, lattices and closure systems: related formalisms and applications (dagstuhl seminar 14201).  Dagstuhl Reports, 4(5):1–26, 2014.
  * [3] B. Al-Saedi, O. Fourdrinyo, E. Grégoire, B. Mazure, and L. Saïs.  About some UP-based polynomial fragments of SAT.  In Annals of Mathematics and Artificial Intelligence, volume 79, pages 25–44. Springer International Publising Switzerland, 2017.
  * [4] J. Álvez, M. Hermo, P. Lucio, and G. Rigau.  Automatic white-box testing of first-order logic ontologies.  J. Log. Comput., 29(5):723–751, 2019.
  * [5] W. W. Armstrong.  Dependency structures of data base relationships.  In Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974, pages 580–583, 1974.
  * [6] V. Arvind and S. Biswas.  An $O(n^{2})$ algorithm for the satisfiability problem of a subset of proposotional sentences in CNF that include all Horn sentences.  Information Processing Letters, 1987.
  * [7] B. Aspvall.  Recognising disguised NR(1) instances of the satisfiability problem.  Journal of Algorithms, (1):97–103, 1980.
  * [8] G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, and R. Sebastiani.  Integrating boolean and mathematical solving: Foundations, basic algorithms, and requirements.  In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors, Artificial Intelligence, Automated Reasoning, and Symbolic Computation, Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 1-5, 2002, Proceedings, volume 2385 of Lecture Notes in Computer Science, pages 231–245. Springer, 2002.
  * [9] G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, and R. Sebastiani.  A SAT based approach for solving formulas over boolean and linear mathematical propositions.  In Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, pages 195–210, 2002.
  * [10] G. Ausiello, P. G. Franciosa, D. Frigioni, and R. Giaccio.  Decremental maintenance of reachability in hypergraphs and minimum models of horn formulae.  In H. W. Leong, H. Imai, and S. Jain, editors, Algorithms and Computation, 8th International Symposium, ISAAC ’97, Singapore, December 17-19, 1997, Proceedings, volume 1350 of Lecture Notes in Computer Science, pages 122–131. Springer, 1997.
  * [11] G. Ausiello and G. F. Italiano.  On-line algorithms for polynomially solvable satisfiability problems.  J. Log. Program., 10(1):69–90, 1991.
  * [12] G. Ausiello and L. Laura.  Directed hypergraphs: Introduction and fundamental algorithms - A survey.  Theor. Comput. Sci., 658:293–306, 2017.
  * [13] L. Bachmair and H. Ganzinger.  Non-clausal resolution and superposition with selection and redundancy criteria.  In Logic Programming and Automated Reasoning,International Conference LPAR’92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pages 273–284, 1992.
  * [14] V. Balabanov and J. R. Jiang.  Unified QBF certification and its applications.  Formal Methods Syst. Des., 41(1):45–65, 2012.
  * [15] T. Balyo, S. Gurský, P. Kučera, and V. Vlček.  On hierarchies over the SLUR class.  In International Symposium on Artificial Intelligence and Mathematics (ISAIM 2012), 2012.
  * [16] C. W. Barrett and J. Donham.  Combining SAT methods with non-clausal decision heuristics.  Electron. Notes Theor. Comput. Sci., 125(3):3–12, 2005.
  * [17] P. Baumgartner.  Model evolution-based theorem proving.  IEEE Intell. Syst., 29(1):4–10, 2014.
  * [18] P. Baumgartner and C. Tinelli.  The model evolution calculus as a first-order DPLL method.  Artif. Intell., 172(4-5):591–632, 2008.
  * [19] B. Beckert, R. Hähnle, and F. Manyà.  The SAT problem of signed CNF formulas.  In D. Basin, M. D’Agostino, D. Gabbay, S. Matthews, and L. Viganò, editors, Labelled Deduction, pages 59–80. Applied Logic Series, vol 17\. Springer, Dordrecht, 2000.
  * [20] M. Ben-Ari.  Mathematical Logic for Computer Science, 3rd Edition.  Springer, 2012.
  * [21] K. Ben-Khalifa and S. Motameny.  Horn representation of a concept lattice.  Int. J. Gen. Syst., 38(4):469–483, 2009.
  * [22] K. Bertet, C. Demko, J. Viaud, and C. Guérin.  Lattices, closures systems and implication bases: A survey of structural aspects and algorithms.  Theor. Comput. Sci., 743:93–109, 2018.
  * [23] K. Bertet and B. Monjardet.  The multiple facets of the canonical direct unit implicational basis.  Theor. Comput. Sci., 411(22-24):2155–2166, 2010.
  * [24] W. Bibel.  On Matrices with Connections.  J. ACM., 28(4):633–645, 1981.
  * [25] M. Bofill, F. Manyà, A. Vidal, and M. Villaret.  The complexity of three-valued Lukasiewicz rules.  In MDAI, pages 221–229, 2015.
  * [26] M. Bofill, F. Manyà, A. Vidal, and M. Villaret.  New complexity results for Lukasiewicz logic.  Soft Computing, 23 (7):2187–2097, 2019.
  * [27] S. Borgwardt, M. Cerami, and R. Peñaloza.  Many-valued horn logic is hard.  In Proceedings of the First Workshop on Logics for Reasoning about Preferences, Uncertainty, and Vagueness, PRUV 2014, co-located with 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Vienna, Austria, July 23-24, 2014, pages 52–58, 2014.
  * [28] E. Boros, Y. Crama, and P. L. Hammer.  Polynomial-time inference of all valid implications for Horn and related formulae.  Annals of Mathematics and Artificial Intelligence, 1:21–32, 1990\.
  * [29] E. Boros, Y. Crama, P. L. Hammer, and M. Saks.  A complexity index for satisfiability problems.  SIAM Journal on Computing, 23:45–49, 1994.
  * [30] A. Bria, W. Faber, and N. Leone.  Normal form nested programs.  Fundam. Informaticae, 96(3):271–295, 2009.
  * [31] F. Bry, N. Eisinger, T. Eiter, T. Furche, G. Gottlob, C. Ley, B. Linse, R. Pichler, and F. Wei.  Foundations of rule-based query answering.  In Reasoning Web, Third International Summer School 2007, Dresden, Germany, September 3-7, 2007, Tutorial Lectures, pages 1–153, 2007\.
  * [32] H. Büning and U. Bubeck.  QBF Theory.  In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability: Chapter 23, pages 339–395. IOS Press, 2009.
  * [33] H. Büning and O. Kullman.  Minimun Unsatisfiability and Autarkies.  In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability: Chapter 11, pages 339–395. IOS Press, 2009.
  * [34] P. Cabalar, J. Fandinno, T. Schaub, and S. Schellhorn.  Gelfond-zhang aggregates as propositional formulas.  Artif. Intell., 274:26–43, 2019.
  * [35] M. Cadoli and F. Scarcello.  Semantical and computational aspects of horn approximations.  Artif. Intell., 119(1-2):1–17, 2000.
  * [36] R. Chandrasekaran.  Integer programming problems for which a simple rounding type of algorithm works.  In Progress in Combinatorial Optimization. Academic Press Canada, Toronto, Ontario, Canada, pages 101–106, 1984.
  * [37] V. Chandru, C. Coullard, P. Hammer, M. Montanuz, and X. Sun.  On renamable Horn and generalised Horn functions.  Annals of Mathematics and Artificial Intelligence, (1):33–47, 1990\.
  * [38] V. Chandru and J. Hooker.  Extended Horn sets in propositional logic.  Journal of ACM, (38):205–221, 1991.
  * [39] E. Chavarria-Baez and X. Li.  Structural error verification in active rule-based systems using petri nets.  In MICAI-06, 2006.
  * [40] K. Claessen, N. Een, M. Sheeran, N. Sörenson, A. Voronov, and K. Akesson.  SAT-Solving in Practice, with a Tutorial Example from Supervisory Control.  Discrete Event Dyn. Syst., 19:495–524, 2009.
  * [41] M. Conforti, G. Cornuéjols, and K. Vusković.  Balanced matrices.  Discrete Mathematics, 306(19-20):2411–2437, 2006.
  * [42] S. Cook.  The complexity of theorem-proving procedures.  In Third ACM Symposium on theory of Computing, pages 151–158, 1971\.
  * [43] Y. Crama and P. L. Hammer.  Boolean Functions - Theory, Algorithms, and Applications, volume 142 of Encyclopedia of mathematics and its applications.  Cambridge University Press, 2011.
  * [44] M. Dalal.  An almost quadratic class of satisfiability problems.  In W. Wahlster, editor, 12th European Conference on Artificial Intelligence, pages 355–359. John Wiley and Sons, Ltd., 1996.
  * [45] M. Dalal and D. Etherington.  A hierarchy of tractable satisfiability problems.  Information Processing Letters, (44):173–180, 1992.
  * [46] E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov.  Complexity and expressive power of logic programming.  ACM Comput. Surv., 33(3):374–425, 2001.
  * [47] A. Darwiche.  Model-based diagnosis using structured system descriptions.  J. Artif. Intell. Res., 8:165–222, 1998.
  * [48] A. Darwiche.  Compiling knowledge into decomposable negation normal form.  In Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99, Stockholm, Sweden, July 31 - August 6, 1999. 2 Volumes, 1450 pages, pages 284–289, 1999.
  * [49] A. Darwiche.  Decomposable negation normal form.  J. ACM, 48(4):608–647, 2001.
  * [50] A. Darwiche and P. Marquis.  A knowledge compilation map.  J. Artif. Intell. Res., 17:229–264, 2002.
  * [51] R. Dechter and J. Pearl.  Structura identifiction in relational data.  Artificial Intelligence, 58, 1992.
  * [52] A. del Val.  Tractable databases: how to make propositional unit resolution complete through compilation.  In Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR’94), pages 551–561, 1994.
  * [53] H. E. Dixon, M. L. Ginsberg, and A. J. Parkes.  Generalizing boolean satisfiability I: background and survey of existing work.  J. Artif. Intell. Res., 21:193–243, 2004.
  * [54] P. Doherty, J. Kachniarz, and A. Szalas.  Meta-queries on deductive databases.  Fundam. Inform., 40(1):7–30, 1999.
  * [55] W. Dowling and J. Gallier.  Linear-time algorithms for testing the satisfiability of propositional Horn formulae.  Journal of Logic Programming, (3):267–284, 1984.
  * [56] R. Drechsler, T. Junttila, and I. Niemelä.  Non-clausal SAT and ATPG.  In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability: Chapter 21, pages 655–693. IOS Press, 2009.
  * [57] V. D’Silva, D. Kroening, and G. Weissenbacher.  A survey of automated techniques for formal software verification.  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7), 2008.
  * [58] D. Dubois, J. Lang, and H. Prade.  Possibilistic logic.  In Handbook of Logic in Artificial Intelligence and Logic Programming, pages 419–513. New York: Oxford University Press, 1994.
  * [59] D. Dubois and H. Prade.  Possibilistic Logic - An Overview.  In J. W. D. M. Gabbay, J. H. Siekmann, editor, Handbook of the History of Logic. Vol 9, Computational Logic, pages 283–342. North-Holland, 2014\.
  * [60] O. Dubois, P. André, Y. Boufkhad, and Y. Carlie.  Chap. SAT vs. UNSAT, volume 26 of Second DIMACS implementation challenge: cliques, coloring and usatisfiability. DIMACS Series in Discrete Mathematics and Theoritical Computer Sciences, pages 415–436.  American Mathematical Society, 1996.
  * [61] U. Egly, M. Seidl, and S. Woltran.  A solver for qbfs in negation normal form.  Constraints An Int. J., 14(1):38–79, 2009.
  * [62] T. Eiter, P. Kilpellainen, and H. Mannila.  Recognizing renamable generalized propositional formulas is NP-complete.  Discrete Applied Mathematics, 59:23–31, 1995.
  * [63] M. Färber and C. Kaliszyk.  Certification of nonclausal connection tableaux proofs.  In Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, pages 21–38, 2019.
  * [64] H. Fargier and P. Marquis.  Extending the knowledge compilation map: Krom, horn, affine and beyond.  In D. Fox and C. P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 442–447. AAAI Press, 2008\.
  * [65] A. Farzan and Z. Kincaid.  Strategy synthesis for linear arithmetic games.  Proc. ACM Program. Lang., 2(POPL):61:1–61:30, 2018.
  * [66] O. Fourdrinoy, E. Grégoire, B. Mazure, and L. Saïs.  Reducing hard SAT instances to polynomial ones.  In Procedings of the IEEE International Conference on Information Reuse and Integration (IRI 2007), pages 18–23, 2007.
  * [67] J. Franco and A. V. Gelder.  A perspective on certain polynomial time solvable classes of satisfiability.  Discrete Applied Mathematics, 125(3):177–214, 2003.
  * [68] J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas.  Invariant-free clausal temporal resolution.  J. Autom. Reasoning, 50(1):1–49, 2013.
  * [69] G. Gallo and M. Scutellà.  Polynomially solvable satisfiability problems.  Inform. Procc. Letters, 29:221–227, 1988.
  * [70] G. Gallo and G. Urbani.  Algorithms for testing the satisfiability of propositional formulae.  Journal of Logic Programming, (7):45–61, 1989.
  * [71] B. Ganter and R. Wille.  Formal Concept Analysis - Mathematical Foundations.  Springer, 1999.
  * [72] M. Ghallab and G. Escalada-Imaz.  A linear control algorithm for a class of rule-based systems.  Journal of Logic Programming, (11):117–132, 1991.
  * [73] E. Giunchiglia and R. Sebastiani.  Applying the davis-putnam procedure to non-clausal formulas.  In AI*IA 99:Advances in Artificial Intelligence, 6th Congress of the Italian Association for Artificial Intelligence, Bologna, Italy, September 14-17, 1999, Proceedings, pages 84–94, 1999.
  * [74] C. D. Giusto, M. Gabbrielli, and M. C. Meo.  On the expressive power of multiple heads in CHR.  ACM Trans. Comput. Log., 13(1):6:1–6:19, 2012.
  * [75] G. Gogic, H. A. Kautz, C. H. Papadimitriou, and B. Selman.  The comparative linguistics of knowledge representation.  In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25 1995, 2 Volumes, pages 862–869. Morgan Kaufmann, 1995.
  * [76] G. Gutiérrez, I. P. de Guzmán, J. Martínez, M. Ojeda-Aciego, and A. Valverde.  Satisfiability testing for boolean formulas using delta-trees.  Studia Logica, 72(1):85–112, 2002.
  * [77] M. Gwynne and O. Kullmann.  Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution.  Journal of Automatic Reasoning, (52):31–65, 2014.
  * [78] M. Hague, A. W. Lin, P. Rümmer, and Z. Wu.  Monadic decomposition in integer linear arithmetic.  In N. Peltier and V. Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 122–140. Springer, 2020.
  * [79] R. Hähnle.  Complexity of Many-Valued Logics.  In Proceedings ISMVL 2001: 137-148, 2001.
  * [80] R. Hähnle, N. V. Murray, and E. Rosenthal.  Linearity and regularity with negation normal form.  Theor. Comput. Sci., 328(3):325–354, 2004.
  * [81] P. L. Hammer and A. Kogan.  Horn functions and their dnfs.  Inf. Process. Lett., 44(1):23–29, 1992.
  * [82] P. L. Hammer and A. Kogan.  Optimal compression of propositional horn knowledge bases: Complexity and approximation.  Artif. Intell., 64(1):131–145, 1993.
  * [83] P. L. Hammer and A. Kogan.  Essential and redundant rules in horn knowledge bases.  Decis. Support Syst., 16(2):119–130, 1996.
  * [84] L. Henschen and L. Wos.  Unit refutations and Horn sets.  Journal of the Association for Computing Machinery, 21(4):590–605, 1974.
  * [85] B. Holen, E. B. Johnsen, and A. Waaler.  Proof search for the first-order connection calculus in maude.  In Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008, pages 173–188, 2008.
  * [86] T. Horiyama and T. Ibaraki.  Reasoning with ordered binary decision diagrams.  Discret. Appl. Math., 142(1-3):151–163, 2004.
  * [87] A. Horn.  On sentences which are of direct unions of algebras.  J. Symb. Logic, 16(1):14–21, 1951.
  * [88] G. E. Imaz.  A First Polynomial Non-Clausal Class in Many-Valued Logic.  CoRR, https://arxiv.org/abs/2110.12901:1–37, 2021.
  * [89] G. E. Imaz.  The Possibilistic Non-Clausal Horn Knowledge Bases.  CoRR, http://arxiv.org/abs/2111.07648:1–43, 2021.
  * [90] A. Itai and J. Makowsky.  On the complexity of Herbrand’s theorem.  Technical Report 243, Dept. of Computer Science, Israel Inst. of Technology, 1982.
  * [91] A. Itai and J. Makowsky.  Unification as a complexity measure for logic programming.  Journal of Logic Programming, (4):105 – 177, 1987.
  * [92] E. K. Jackson and W. Schulte.  Model generation for horn logic with stratified negation.  In K. Suzuki, T. Higashino, K. Yasumoto, and K. El-Fakih, editors, Formal Techniques for Networked and Distributed Systems - FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June 10-13, 2008, Proceedings, volume 5048 of Lecture Notes in Computer Science, pages 1–20. Springer, 2008.
  * [93] H. Jain, C. Bartzis, and E. Clarke.  Satisfiability Checking of Non-clausal Formulas Using General Matings.  In SAT-2006, pages 75–89, 2006.
  * [94] H. Jain and E. M. Clarke.  Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts.  In Proceedings of the 46th Design Automation Conference, DAC 2009, San Francisco, CA, USA, July 26-31, 2009, pages 563–568, 2009.
  * [95] S. Jha, R. Limaye, and S. A. Seshia.  Beaver: Engineering an efficient SMT solver for bit-vector arithmetic.  In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, pages 668–674, 2009.
  * [96] H. Kautz, B. Selman, and D. McAllester.  Exploiting variable dependency in local search.  In Abstracts of the Poster Session of IJCAI-97, 1997.
  * [97] H. A. Kautz, M. J. Kearns, and B. Selman.  Reasoning with characteristic models.  In R. Fikes and W. G. Lehnert, editors, Proceedings of the 11th National Conference on Artificial Intelligence. Washington, DC, USA, July 11-15, 1993, pages 34–39. AAAI Press / The MIT Press, 1993.
  * [98] H. A. Kautz and B. Selman.  Forming concepts for fast inference.  In Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, USA, July 12-16, 1992, pages 786–793, 1992.
  * [99] S. Klarman, U. Endriss, and S. Schlobach.  Abox abduction in the description logic _ALC_.  J. Autom. Reasoning, 46(1):43–80, 2011.
  * [100] H. Kleine Büning, M. Karpinski, and A. Flögel.  Resolution for quantified boolean formulas.  Inf. Comput., 117(1):12–18, 1995.
  * [101] A. Komuravelli, N. Bjørner, A. Gurfinkel, and K. L. McMillan.  Compositional verification of procedural programs using horn clauses over integers and arrays.  In R. Kaivola and T. Wahl, editors, Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015, pages 89–96. IEEE, 2015.
  * [102] E. Kotelnikov, L. Kovács, M. Suda, and A. Voronkov.  A clausal normal form translation for FOOL.  In C. Benzmüller, G. Sutcliffe, and R. Rojas, editors, GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19 - October 2, 2016, Berlin, Germany, volume 41 of EPiC Series in Computing, pages 53–71. EasyChair, 2016.
  * [103] M. Koubarakis and S. Skiadopoulos.  Querying temporal and spatial constraint networks in PTIME.  Artif. Intell., 123(1-2):223–263, 2000.
  * [104] O. Kullmann.  Investigations on autark assignments.  Discrete Applied Mathematics, 107:99–137, 2000.
  * [105] O. Kullmann.  Lean clause-sets: generalizations of minimally unsatisfiable clause-sets.  Discrete Applied Mathematics, 130(2):209–249, 2003.
  * [106] J. Lang.  Possibilistic logic: complexity and algorithms.  In e. Gabbay D., Smets Ph, editor, Handbook of Defeasible Reasoning and Uncertainty Management System, pages 179–220. Dordrecht, The Netherlands: Kluwer Academic Publishers, 2001.
  * [107] H. Lewis.  Renaming a set of clauses as a Horn set.  Journal of the ACM, (25):134–135, 1978.
  * [108] C. M. Li and F. Manyà.  MaxSAT, Hard and Soft Constraints.  In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability: Chapter 9, pages 613–631. IOS Press, 2009.
  * [109] C. M. Li, F. Manyà, and J. Planes.  New inference rules for Max-SAT.  Journal of Artificial Intelligence Research (JAIR), (1):134–135, 2007.
  * [110] C. M. Li, F. Manyà, and J. R. Soler.  A tableau calculus for non-clausal maximum satisfiability.  In Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, pages 58–73, 2019.
  * [111] V. Lifschitz, L. R. Tang, and H. Turner.  Nested expressions in logic programs.  Ann. Math. Artif. Intell., 25(3-4):369–389, 1999.
  * [112] H. Liu, Q. Lin, L. Mao, and Z. Zhang.  Dynamic adaptive fuzzy petri nets for knowledge representation and reasoning.  IEEE Trans. Syst. Man Cybern. Syst., 43(6):1399–1410, 2013.
  * [113] F. Lonsing and A. Biere.  Nenofex: Expanding NNF for QBF solving.  In Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008\. Proceedings, pages 196–210, 2008.
  * [114] K. Makino and H. Ono.  Deductive inference for the interiors and exteriors of horn theories.  ACM Trans. Comput. Log., 13(3):23:1–23:16, 2012.
  * [115] J. McKinsey.  The decision problem for some classes of sentences without quantifiers.  Journal of Symbolic Logic, (8):61–76, 1943.
  * [116] A. Meier and V. Sorge.  A new set of algebraic benchmark problems for SAT solvers.  In In SAT, pages 459–466, 2005.
  * [117] M. Minoux.  LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation.  Information Processing Letters, (29):1–12, 1988.
  * [118] R. Muhammad and P. J. Stuckey.  A stochastic non-cnf SAT solver.  In Q. Yang and G. I. Webb, editors, PRICAI 2006: Trends in Artificial Intelligence, 9th Pacific Rim International Conference on Artificial Intelligence, Guilin, China, August 7-11, 2006, Proceedings, volume 4099 of Lecture Notes in Computer Science, pages 120–129. Springer, 2006.
  * [119] N. Murray.  Completely Non-Clausal Theorem Proving.  Artificial Intelligence, 18(1):67–85, 1982.
  * [120] N. V. Murray and E. Rosenthal.  On the relative merits of path dissolution and the method of analytic tableaux.  Theor. Comput. Sci., 131(1):1–28, 1994.
  * [121] J. Navarro and A. Voronkov.  Generation of Hard Non-Clausal Random Satisfiability Problems.  In The Twentieth National Conference on Artificial Intelligence, pages 426–436, 2005.
  * [122] J. C. Nieves and H. Lindgren.  Possibilistic nested logic programs.  In Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary, pages 267–276, 2012.
  * [123] T. Nipkow.  Linear quantifier elimination.  J. Autom. Reasoning, 45(2):189–212, 2010.
  * [124] B. E. Oliver and J. Otten.  Equality preprocessing in connection calculi.  In Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual), pages 76–92, 2020.
  * [125] J. Otten.  On the advantage of a non-clausal davis-putnam procedure.  Technical report, Technische Hochschule Darmstadt, Geramny, 1997.
  * [126] J. Otten.  A non-clausal connection calculus.  In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings, pages 226–241, 2011.
  * [127] D. Pearce.  Equilibrium logic.  Ann. Math. Artif. Intell., 47(1-2):3–41, 2006.
  * [128] D. Pearce, H. Tompits, and S. Woltran.  Characterising equilibrium logic and nested logic programs: Reductions and complexity${}^{\mbox{, }}$.  Theory Pract. Log. Program., 9(5):565–616, 2009.
  * [129] D. Petrolani.  A linear algorithm for unique Horn satisfiability.  Information Processing Letters, 48(2):61–66, 1993.
  * [130] D. Petrolani.  Hierarchies of polynomially solvable satisfiability problems.  Annals of Mathematics and Artificial Intelligence, 17:339–357, 1996\.
  * [131] A. Platzer.  Differential dynamic logic for hybrid systems.  J. Autom. Reason., 41(2):143–189, 2008.
  * [132] A. Ramesh, B. Beckert, R. Hähnle, and N. V. Murray.  Fast subsumption checks using anti-links.  J. Automated Reasoning, 18(1):47–83, 1997.
  * [133] E. Scala, P. Haslum, S. Thiébaux, and M. Ramírez.  Subgoaling techniques for satisficing and optimal numeric planning.  J. Artif. Intell. Res., 68:691–752, 2020.
  * [134] J. S. Schlipf, F. Annexstein, J. Franco, and R. Swaminathan.  On finding solutions for extended Horn formulas.  Information Processing Letters, (54):133–137, 1995.
  * [135] M. Scutellà.  A note on Dowling and Gallier’s top-down algorithm for propositional Horn satisfiability.  Journal of Logic Programming, (8):265–273, 1990.
  * [136] R. Sebastiani.  Applying GSAT to non-clausal formulas (research note).  J. Artif. Intell. Res., 1:309–314, 1994.
  * [137] B. Selman and H. A. Kautz.  Knowledge compilation using horn approximations.  In Proceedings of the 9th National Conference on Artificial Intelligence, Anaheim, CA, USA, July 14-19, 1991, Volume 2, pages 904–909, 1991\.
  * [138] B. Selman and H. A. Kautz.  Knowledge compilation and theory approximation.  J. ACM, 43(2):193–224, 1996.
  * [139] B. Selman, H. A. Kautz, and B. Cohen.  Noise strategies for improving local search.  In Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31 - August 4, 1994, Volume 1, pages 337–343, 1994.
  * [140] B. Selman, H. J. Levesque, and D. G. Mitchell.  A new method for solving hard satisfiability problems.  In Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, USA, July 12-16, 1992, pages 440–446, 1992.
  * [141] Z. Stachniak.  Non-Clausal Reasoning with Definite Theories.  Fundamenta Informaticae, 48:1–26, 2001.
  * [142] Z. Stachniak.  Going Non-clausal.  In Fifth International Symposium on the Theory and Applications of Satisfiability Testing, pages 316–322, 2002.
  * [143] K. Subramani and J. Worthington.  Feasibility checking in horn constraint systems through a reduction based approach.  Theor. Comput. Sci., 576:1–17, 2015.
  * [144] R. P. Swaminathan and D. K. Wagner.  The arborescence realization problem.  Discrete Applied Mathematics, (59):267–283, 1995.
  * [145] N. Tamura, A. Taga, S. Kitagawa, and M. Banbara.  Compiling finite linear CSP into SAT.  Constraints An Int. J., 14(2):254–272, 2009.
  * [146] C. Thiffault, F. Bacchus, and T. Walsh.  Solving Non-Clausal Formulas with DPLL search.  In Tenth International Conference on Principles and Practice of Constraint Programming, pages 663–678, 2004.
  * [147] C. A. Tovey.  A simplified NP-complete satisfiability problem.  Discrete Applied Mathematics, 8:85–89, 1984.
  * [148] G. Tseitin.  On the complexity of proofs in propositional logics.  In J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic, pages 466–483. Springer, 1983.
  * [149] H. Unno, Y. Satake, T. Terauchi, and E. Koskinen.  Program verification via predicate constraint satisfiability modulo theories.  CoRR, abs/2007.03656, 2020.
  * [150] H. Unno and T. Terauchi.  Inferring simple solutions to recursion-free horn clauses via sampling.  In C. Baier and C. Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pages 149–163. Springer, 2015.
  * [151] H. van Maaren.  A short note on some tractable classes of the satisfiability problem.  Information and Computation, 158(2):125–130, 2000.
  * [152] O. Čepek and P. Kučera.  Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing.  Discrete Applied Mathematics, 149(1-3):14–52, 2005.
  * [153] O. Čepek, P. Kučera, and V. Vlček.  Properties of SLUR formulae.  In Springer, editor, SOFSEM 2012: Theory and Practices of Computer Science. LNCS., volume 7147, pages 177–189. Bieliková M., Friedich G., Gottlob G. Katzenbeisser S., Turán G., 2012.
  * [154] M. Veksler and O. Strichman.  Learning general constraints in CSP.  Artif. Intell., 238:135–153, 2016.
  * [155] D. S. Warren.  Top-down and bottom-up evaluation procedurally integrated.  Theory Pract. Log. Program., 18(3-4):706–721, 2018.
  * [156] M. Wild.  The joy of implications, aka pure horn formulas: Mainly a survey.  Theor. Comput. Sci., 658:264–292, 2017.
  * [157] P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta.  Combining decision diagrams and SAT procedures for efficient symbolic model checking.  Computer Aided Verification (CAV), LNCS. Vol. 1855, pages 124–138, 2000.
  * [158] P. J. Wojciechowski.  Analyzing Satisfiability and Refutatibility in Selected Constraint Systems.  PhD thesis, West Virginia University, 2019.
  * [159] Y. Xu, J. Liu, X. He, X. Zhong, and S. Chen.  Non-clausal multi-ary $\alpha$-generalized resolution calculus for a finite lattice-valued logic.  Int. J. Comput. Intell. Syst., 11(1):384–401, 2018.
  * [160] S. Yamasaki and S. Doshita.  The satisfiability problem for a class consisting of Horn sentences and some non-Horn sentences in propositional logic.  Inform. Control, 59:1–12, 1983.
  * [161] S. J. H. Yang, J. J. P. Tsai, and C. Chen.  Fuzzy rule base systems verification using high-level petri nets.  IEEE Trans. Knowl. Data Eng., 15(2):457–473, 2003.