Ground joinability and connectedness in the superposition calculus
type: Item
instance of: scholarly article
title: Ground joinability and connectedness in the superposition calculus
DOI: 10.1007/978-3-031-10769-6_11
author: André Duarte
author: Konstantin Korovin
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628187
zbMATH Keywords: superposition
zbMATH Keywords: ground joinability
zbMATH Keywords: connectedness
zbMATH Keywords: closure redundancy
zbMATH Keywords: first-order theorem proving
describes a project that uses: MadMax
describes a project that uses: iProver
describes a project that uses: Twee
describes a project that uses: VAMPIRE
describes a project that uses: Waldmeister
describes a project that uses: TPTP
describes a project that uses: E Theorem Prover
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 11
OpenAlex ID: W4289104029
cites work: On using ground joinable equations in equational theorem proving
cites work: Term Rewriting and All That
cites work: Critical pair criteria for completion
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Basic paramodulation
cites work: An asymptotic equivalent for the number of total preorders on a finite set
cites work: Efficient encodings of first-order Horn formulas in equational logic
cites work: Proving termination with multiset orderings
cites work: Implementing Superposition in iProver (System Description)
cites work: AC simplifications and closure redundancies in the superposition calculus
cites work: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
cites work: Q5581665
cites work: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
cites work: Paramodulation-based theorem proving
cites work: System Description: E 1.8
cites work: Twee: an equational theorem prover
cites work: The CADE-14 ATP system competition
cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
cites work: A comprehensive framework for saturation theorem proving
cites work: MædMax: a maximal ordered completion tool
cites work: Ordered rewriting and confluence
description: scientific article; zbMATH DE number 7628187