Superposition theorem proving for abelian groups represented as integer modules

被引：8

作者：

Stuber, J ^{[1
]}

机构：

[1] Max Planck Informat, D-66123 Saarbrucken, Germany

来源：

THEORETICAL COMPUTER SCIENCE | 1998年 / 208卷 / 1-2期

关键词：

abelian groups; paramodulation; ordering restrictions; automated theorem proving; superposition;

D O I：

10.1016/S0304-3975(98)00082-6

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We define a refutationally complete superposition calculus specialized for abelian groups represented as integer modules. Compared to a standard superposition prover which applies the axioms directly our calculus substantially reduces the number of inferences. We also investigate situations where the axioms give rise to variable overlaps and we develop techniques to avoid these explosive cases. (C) 1998-Elsevier Science B.V. All rights reserved.

引用

页码：149 / 177

页数：29