报告题目: Automated Deduction in Ring and Group Theory（环论与群论中的自动推理）
报 告 人：张扬 教授（曼尼托巴大学）
时 间：2026年5月8日 15：30
地 点：旭日教学大楼328会议室
摘 要:
Pover9/Mace4 or its predecessor Otter is one of powerful automated theorem provers for the first-order and equational logic. In this talk, we explore various possibilities of using Prover9 in ring and group theory, in particular, rings with involutions, semirings/semigroups with cancellation laws, and near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson's commutativity theorem, give some new proofs, and also present some new results.
