Superposition decides the first-order logic fragment over ground theories
type: Item
instance of: scholarly article
title: Superposition decides the first-order logic fragment over ground theories
zbMATH Open document ID: 1262.68160
author: E. V. Kruglov
author: Christoph Weidenbach
published in: Mathematics in Computer Science
publication date: 2013-04-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 6157646
zbMATH Keywords: theorem proving
zbMATH Keywords: combination of theories
zbMATH Keywords: decision procedure
zbMATH Keywords: arithmetic
describes a project that uses: YAGO
MaRDI profile type: Publication
full work available at URL: s11786-012-0135-4
OpenAlex ID: W2035045326
cites work: Superposition Modulo Linear Arithmetic SUP(LA)
cites work: New results on rewrite-based satisfiability procedures
cites work: A rewriting approach to satisfiability procedures.
cites work: Term Rewriting and All That
cites work: Q4282593
cites work: Refutational theorem proving for hierarchic first-order theories
cites work: (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
cites work: On deciding satisfiability by theorem proving with speculative inferences
cites work: Orderings for term-rewriting systems
cites work: Proving termination with multiset orderings
cites work: Superposition Modulo Non-linear Arithmetic
cites work: Superposition-Based Analysis of First-Order Probabilistic Timed Automata
cites work: Automatic Generation of Invariants for Circular Derivations in SUP(LA)
cites work: Superposition as a decision procedure for timed automata
cites work: Modular proof systems for partial functions with Evans equality
cites work: On Local Reasoning in Verification
cites work: Q3838762
cites work: Integrating Linear Arithmetic into Superposition Calculus
cites work: Solving SAT and SAT Modulo Theories
cites work: Q3506045
cites work: On the Saturation of YAGO
cites work: Q4539608
cites work: Combining superposition, sorts and splitting
DOI: 10.1007/S11786-012-0135-4
description: scientific article; zbMATH DE number 6157646