Automated proofs of equality problems in Overbeek's competition

DOI10.1007/BF00881872zbMath0802.68132MaRDI QIDQ1319385

Han-Tao Zhang

Publication date: 12 April 1994

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

equational reasoningautomated theorem proving

Mathematics Subject Classification ID

Related Items (1)

Uniform strategies: The CADE-11 theorem proving contest

Uses Software

• OTTER
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Problem corner: Robbins algebra: Conditions that make a near-Boolean algebra Boolean
• Automated proofs of the Moufang identities in alternative rings
• A case study in automated theorem proving: Finding sages in combinatory logic
• Termination of rewriting
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic
• Problem corner: Proving equivalence of different axiomatizations of free groups
• Problem corner: Reasoning about equality
• Solving open problems in right alternative rings with Z-module reasoning
• Another single law for groups
• Complete Sets of Reductions for Some Equational Theories

This page was built for publication: Automated proofs of equality problems in Overbeek's competition