### Abstract

We provide a formalization of a variant of the superposition calculus, together with formal proofs of soundness and refutational completeness (w.r.t. the usual redundancy criteria based on clause ordering). This version of the calculus uses all the standard restrictions of the superposition rules, together with the following refinement, inspired by the basic superposition calculus: each clause is associated with a set of terms which are assumed to be in normal form -- thus any application of the replacement rule on these terms is blocked. The set is initially empty and terms may be added or removed at each inference step. The set of terms that are assumed to be in normal form includes any term introduced by previous unifiers as well as any term occurring in the parent clauses at a position that is smaller (according to some given ordering on positions) than a previously replaced term. The standard superposition calculus corresponds to the case where the set of irreducible terms is always empty.

### License

BSD License

### Topics

- Logic/Proof theory

### Session SuperCalc

- multisets_continued
- well_founded_continued
- terms
- equational_clausal_logic
- superposition

## Cite

×

SuperCalc-AFP

    @article{SuperCalc-AFP,
      author  = {Nicolas Peltier},
      title   = {A Variant of the Superposition Calculus},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/SuperCalc.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Sep 6, 2016 : Isabelle2016