Equality Reasoning in Sequent-Based Calculi

Anatoli Degtyarev, Andrei Voronkov

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution


This chapter describes automated reasoning techniques for all main sequent-based methods of automated deduction, including the tableau method, the connection method, model elimination, and the inverse method. It illustrates main results and ideas on the tableau method and sometimes on the inverse method (as a typical backward and a typical forward proof search methods in sequent calculi). The chapter covers the following topics: methods of proof-search in sequent calculi; early history of sequent-based automated deduction; translation of logic with equality into logic without equality; theorem proving using simultaneous rigid E-unification; tableau calculi with rigid paramodulation/superposition; the equality elimination method; and equality reasoning in nonclassical logics. Due to the rapidly growing interest in tableau-based theorem proving, and because the usual techniques of handling equality in automated reasoning do not straightforwardly generalize to tableaux, it is believed that equality reasoning in tableaux and related procedures will be among the central topics in automated deduction in the nearest future. Many new results are presented that have not yet been presented in any systematic way. The chapter introduces the reader in the area of equality reasoning. It introduces the main notation used in the chapter and discusses the standard axiomatization of equality. The chapter then considers several techniques of handling equality in resolution-based procedures and discusses various versions of the paramodulation rule.
Original languageEnglish
Title of host publicationHandbook of Automated Reasoning
EditorsAlan Robinson, Andrei Voronkov
Place of PublicationAmsterdam
PublisherElsevier B.V.
Number of pages96
ISBN (Print)0262182211 , 9780262182218 , 9780444508133
Publication statusPublished - 2001


Dive into the research topics of 'Equality Reasoning in Sequent-Based Calculi'. Together they form a unique fingerprint.

Cite this