ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
The equality axioms are not independent
Full text PdfPdf (156 KB)
Source ACM SIGACT News archive
Volume 35 ,  Issue 3  (September 2004) table of contents
Pages: 98 - 101  
Year of Publication: 2004
ISSN:0163-5700
Author
Dafa Li  Tsinghua University, Beijing, China
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 3,   Downloads (12 Months): 16,   Citation Count: 0
Additional Information:

abstract   references  

Tools and Actions: Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/1027914.1027916
What is a DOI?

ABSTRACT

After computer experiments by using the ANDP prover we showed that the five axioms for reflexivity, symmetry, transitivity and substitutivity of equality can be replaced by only two of the five axioms.


REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
 
2
Li Dafa, Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving, Journal of Automated Reasoning, v.18 n.1, p.105-134, February 1997  [doi>10.1023/A:1005749401809]

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player