This note presents purely mechanical proofs of the Levi commutator problem in group theory. The problem was solved first by using the theorem prover EQP, developed by William McCune at the Argonne National Laboratory. The fastest proof was found by using Peers-mcd, the Clause-Diffusion parallelization of EQP, developed by the author at the University of Iowa.

Mechanical proofs of the Levi commutator problem

BONACINA, Maria Paola
1998-01-01

Abstract

This note presents purely mechanical proofs of the Levi commutator problem in group theory. The problem was solved first by using the theorem prover EQP, developed by William McCune at the Argonne National Laboratory. The fastest proof was found by using Peers-mcd, the Clause-Diffusion parallelization of EQP, developed by the author at the University of Iowa.
1998
Automated theorem proving; contraction-based theorem proving; Distributed deduction
File in questo prodotto:
File Dimensione Formato  
PSM-CADE1998LeviCommut.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 116.42 kB
Formato Adobe PDF
116.42 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/16063
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact