3 papers
math.GR2015
Loops with abelian inner mapping groups: An application of automated deduction
Michael Kinyon, Robert Veroff, Petr Vojtěchovský
We describe a large-scale project in applied automated deduction concerned with the following problem of considerable interest in loop theory: If is a loop with commuting inner…
math.LO2003
Yet Another Single Law for Lattices
William McCune, Ranganathan Padmanabhan, Robert Veroff
In this note we show that the equational theory of all lattices is defined by a single absorption law. The identity of length 29 with 8 variables is shorter than previously known s…
cs.LO2003
Double-Negation Elimination in Some Propositional Logics
Michael Beeson, Robert Veroff, Larry Wos
This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none…