International Joint Conference on Artificial Intelligence · 1993 · 85 citations · 3 references
ComputingComputer ScienceMathematicsAlgebraParallel ComputingTheory Of ComputationAbstract AlgebraData ParallelismGroup TheoryParallel ComputationProof AssistantsTheorem ProvingAutomated Theorem Proving In AlgebraComputational Group TheoryMechanized ProofsParallel Data ProcessingParallel InferenceParallel ProcessingProof GenerationProof Production
This is a report of the application of the Model Generation Theorem Prover developed at ICOT to problems in the theory of finite quasigroups. Several of the problems were previously open. In this paper, we discuss our theorem proving methods, related to those of the existing provers SATCHMO (Manthey, Bry) and OTTER (McCune), and note how parallel processing on the ICOT Parallel Inference Machines was used to obtain high speeds. We then present and discuss our machine-aided investigation of seven problems concerning the existence of types of quasigroup.
3