I am currently writing a paper about automated theorem proving in first-order logic. Equality is not uncommon for mathematical problems and almost every theorem prover like VAMPIRE or SPASS has a calculus for equality. But the most paper are always writing about the term "superposition" calculus. A simple google search did not help to find any information about this term, only the wikipedia website which means "it can be used for first-order logic with equality".

Another paper referneced to the Paramodulation-based theorem proving which describes the concept of paramodulation for theorem proving. It seems that the superposition is some modified version of paramodulation, but I don't understand why and in which way.

So, is there any explanation of this calculus or can someone give me some hints what is different from paramodulation?


1 Answer 1


This is late for you, but probably might be of help to others. I myself had asked this question and I wrote the summary of my findings to the acl2-help mailing list on 8 and 9 September 2013: https://utlists.utexas.edu/sympa/arc/acl2-help/2013-09/msg00005.html https://utlists.utexas.edu/sympa/arc/acl2-help/2013-09/msg00006.html

Disclaimer: What follows is my understanding of the subject and I am not an expert.

I assume you are familiar with what is called term-rewriting. Informally its a very simple notion where one uses a rule to reduce or rewrite another expression.

A rewrite rule is usually a universally quantified formula of the form $C \Rightarrow l=r$, where $C$ is a formula and $l$ and $r$ are terms. One says that a rule $R$ applies to another formula $\Phi$, if there is some subterm $s$ of $\Phi$ and some substitution $\sigma$ such that $l\sigma = s$ (this process is called matching) and $C\sigma$ is true. If $R$ applies to $\Phi$, then one can rewrite $\Phi$ to $\Phi\sigma$. Demodulation is another name for unconditional term-rewriting, i.e., $C$ is simply true and so $R$ is just $l=r$.

Rewriting involves matching,i.e., one-way unification. Paramodulation involves full unification. Moreover, the equality ($l=r$) that is used to perform paramodulation, is not directed, either lhs or rhs can be unified with a subterm in the other literal paramodulated upon.

Superposition is a restriction of Paramodulation. In particular, the rules of inference named 'Superposition (left/right)' are restrictions of "ordered" paramodulation, i.e., the paramodulation rule is applied only when equation $l=r$ (to be instantiated/unified) satisfies certain properties: $l >> r$ for a given reduction order $>>$, $l=r$ is maximal (wrt $>>$) in the clause etc etc.

Here are some fundamental papers that are interesting from a historical point of view.

[1] The concept of demodulation in theorem proving - L Wos, GA Robinson, DF Carson, L Shalla - Journal of the ACM (JACM), 1967

[2] Handbook of Logic and Automated Reasoning - J Harrison.

[3] Paramodulation and theorem-proving in first-order theories with equality- G Robinson, L Wos - Machine intelligence, 1969

[4] Rewrite-based equational theorem proving with selection and simplification - L Bachmair, H Ganzinger - Journal of Logic and Computation, 1994

[5] Simple word problems in universal algebras - DE Knuth, PB Bendix - Computational problems in abstract algebra 1970

[6] A superposition oriented theorem prover - L Fribourg - Theoretical Computer Science, 1985 - Elsevier

[7] Completion without failure - L Bachmair, N Dershowitz, DA Plaisted -1989

  • 1
    $\begingroup$ Welcome to the site! Good answers to older questions are always appreciated. One of the goals of the site is to be useful to anybody who might be wondering about a question, not just the person who originally asked it, so your first sentence is exactly right. :-) $\endgroup$ May 17, 2017 at 9:02
  • $\begingroup$ That's very helpful, thank you. The two links are dead. Any chance you could revive them? $\endgroup$
    – Metaxal
    Aug 7, 2020 at 12:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.