Subsumption demodulation in first-order theorem proving
type: Item
instance of: scholarly article
title: Subsumption demodulation in first-order theorem proving
DOI: 10.1007/978-3-030-51074-9_17
author: Bernhard Gleiss
author: Laura Kovács
author: Jakob Rath
publication date: 2022-11-09T00:00:00Z
full work available at URL: https://arxiv.org/abs/2001.10213
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7614519
describes a project that uses: SPASS
describes a project that uses: CVC4
describes a project that uses: StarExec
describes a project that uses: AVATAR
describes a project that uses: TPTP
describes a project that uses: VAMPIRE
describes a project that uses: SMT-LIB
describes a project that uses: z3
describes a project that uses: GNU parallel
MaRDI profile type: Publication
OpenAlex ID: W3038385067
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Resolution theorem proving
cites work: Horn Clause Solvers for Program Verification
cites work: Computer Aided Verification
cites work: From Search to Computation: Redundancy Criteria and Simplification at Work
cites work: Paramodulation-based theorem proving
cites work: Scaling up DPLL(T) string solvers using context-dependent simplification
cites work: Faster, higher, stronger: E 2.3
cites work: Term indexing
cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
cites work: AVATAR: The Architecture for First-Order Theorem Provers
cites work: Combining superposition, sorts and splitting
cites work: Subterm contextual rewriting
description: scientific article; zbMATH DE number 7614519