English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)

Ganzinger, H., & Waldmann, U. (1996). Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). In M. A. McRobbie, & J. K. Slaney (Eds.), Proceedings of the 13th International Conference on Automated Deduction (CADE-13) (pp. 388-402). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Ganzinger, Harald1, Author           
Waldmann, Uwe1, 2, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 Abstract: Cancellative abelian monoids encompass abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Both the AC axioms and the cancellation law are difficult for a general purpose theorem prover, as they create many variants of clauses which contain sums. We describe a refined superposition calculus for cancellative abelian monoids which requires neither explicit inferences with the theory clauses nor extended equations or clauses. Strong ordering constraints allow us to restrict to inferences that involve the maximal term of the maximal sum in the maximal literal. Besides, the search space is reduced drastically by variable elimination techniques.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121996
 Publication Status: Issued
 Pages: -
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519898
Other: Local-ID: C1256104005ECAFC-D3B31BC55873B750C12564610057884F-GanzingerWaldmann1996CADE
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: New Brunswick, USA
Start-/End Date: 1996

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of the 13th International Conference on Automated Deduction (CADE-13)
Source Genre: Proceedings
 Creator(s):
McRobbie, Michael A., Editor
Slaney, John K., Editor
Affiliations:
-
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 388 - 402 Identifier: ISBN: 3-540-61511-3

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -