Ph.D., Northwestern University, 1980
Primary Research Interest: automated deduction
Some Links for Automated Deduction
recent applications
 AIM problem in loop theory (in progress)
 Simple
axiom systems for Boolean algebra (updated August 27, 2021)
 Challenge problems
with condensed detachment
(updated May 8, 2011)
 Generalized
MV algebras
(updated February 1, 2010)
 Whitehead
and Russell dependency
(updated October 25, 2008)
 Basarab's Theorem in loop theory
(updated June 23, 2007)
 Median algebra
(updated September 28, 2006)
 A firstorder
proof for HBCK (updated September 11, 2005)
 A new result for
modular ortholattices (updated February 17, 2005)
 Robbins algebra
(updated June 21, 2002)
 Simple axiom
systems for lattice theory (updated March 20, 2002)
forums
 JAR,
Journal of Automated Reasoning
 AAR,
Association for Automated Reasoning
 CADE,
Conference on Automated Deduction
 IJCAR,
International Joint Conference on Automated Reasoning
 ADAM,
Automated Deduction and its Application to Mathematics (workshop)
provers
miscellaneous
Personal
Books

P. Helman and R. Veroff,
Intermediate Problem Solving and Data Structures: Walls and Mirrors,
Benjamin Cummings Publishing Company, Menlo Park, California, 1986.

P. Helman and R. Veroff,
Walls and Mirrors: Intermediate Problem Solving and Data Structures
(Modula2 Edition),
Benjamin Cummings Publishing Company, Menlo Park, California, 1988.

R. Veroff (ed.),
Automated Reasoning and Its Applications: Essays in Honor of Larry Wos,
MIT Press, Cambridge, Massachusetts, 1997.

F. Carrano, P. Helman and R. Veroff,
Data Abstraction and Problem Solving with C++: Walls and Mirrors
(Second Edition),
AddisonWesley, Reading, Massachusetts, 1998.
Recent Papers

P. Helman and R. Veroff,
The Application of Automated Reasoning to Formal Models
of Combinatorial Optimization,
Applied Mathematics and Computation, 120(13):175194, 2001.
(postscript)

R. Veroff,
Finding Shortest Proofs: An Application of Linked Inference Rules,
Journal of Automated Reasoning, 27(2):123139, 2001.
(postscript)

R. Veroff,
Solving Open Questions and Other Challenge Problems Using Proof Sketches,
Journal of Automated Reasoning, 27(2):157174, 2001.
(postscript)

W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist and L. Wos,
Short Single Axioms for Boolean Algebra,
Journal of Automated Reasoning, 29(1):116, 2002.
(pdf)

L. Wos, R. Veroff and G. Pieper,
Logical Basis for the Automation of Reasoning: Case Studies,
Tech. Report TRCS200220,
Computer Science Department, University of New Mexico, 2002.
(gzipped postscript,
pdf)

R. Veroff,
Solution to a Challenge Problem in HBCK,
Tech. Report TRCS200232,
Computer Science Department, University of New Mexico, 2002.
(gzipped postscript,
pdf)

R. Veroff,
A Shortest 2Basis for Boolean Algebra in Terms of the Sheffer Stroke,
Journal of Automated Reasoning, 31(1):19, 2003.
(postscript,
pdf)

W. McCune, R. Padmanabhan and R. Veroff,
Yet Another Single Law for Lattices,
Algebra Universalis, 50(2):165169, 2003.
(postscript,
pdf)

W. McCune, R. Padmanabhan, M. A. Rose and R. Veroff,
Short Equational Bases for Ortholattices,
Tech. Report TRCS200401,
Computer Science Department, University of New Mexico, 2004.
(pdf)

W. McCune, R. Padmanabhan, M. A. Rose and R. Veroff,
Short Equational Bases for Ortholattices: Proofs and Countermodels,
Tech. Report TRCS200402,
Computer Science Department, University of New Mexico, 2004.
(pdf)

P. Helman, R. Veroff, S. Atlas and C. Willman,
A Bayesian Network Classification Methodology for Gene Expression Data,
Journal of Computational Biology, 11(4):581615, 2004.
(pdf)

R. Veroff and M. Spinks,
On a Homomorphism Property of Hoops,
Bulletin of the Section of Logic, 33(3):135142, 2004.
(pdf)

W. McCune, R. Padmanabhan, M. A. Rose and R. Veroff,
Automated Discovery of Single Axioms for Ortholattices,
Algebra Universalis, 52(4):541549, 2005.
(pdf,
Web support)

M. Beeson, R. Veroff and L. Wos,
Double Negation Elimination in Some Propositional Logics,
Studia Logica, 80:195234, 2005.
(pdf)

R. Padmanabhan, W. McCune and R. Veroff.
Levi's Commutator Theorems for Cancellative Semigroups.
Semigroup Forum, 71:152157, 2005.
(pdf,
Web support)

M. Spinks and R. Veroff.
On the Equational Definability of BrouwerZadeh Lattices.
Tech. Report TRCS200612,
Computer Science Department, University of New Mexico, 2006.
(pdf)

R. Veroff and M. Spinks.
Axiomatizing the Skew Boolean Propositional Calculus.
Journal of Automated Reasoning, 37(1,2):320, 2006.
(pdf,
errata)

R. Padmanabhan, W. McCune and R. Veroff.
Lattice Laws Forcing Distributivity Under Unique Complementation.
Houston Journal of Mathematics, 33(2):391401, 2007.
(pdf,
Web support)

F. Gilfeather,
V. Hamine.
P. Helman,
J. Hutt,
T. Loring,
C. R. Lyons and
R. Veroff.
Learning and Modeling Biosignatures from Tissue Images.
Computers in Biology and Medicine, 37:15391552, 2007.

M. Spinks and R. Veroff.
Characterisations of Nelson Algebras.
Revista de la Union Matematica Argentina, 48(1):2739, 2007.
(pdf)

M. Spinks and R. Veroff.
Constructive Logic with Strong Negation is a Substructural Logic. I.
Studia Logica, 88(3):325348, 2008.
(Web support,
SpringerLink)

M. Spinks and R. Veroff.
Constructive Logic with Strong Negation is a Substructural Logic. II.
Studia Logica, 89(3):401425, 2008.
(Web support,
SpringerLink)

F. Paoli, M. Spinks and R. Veroff.
Abelian Logic and the Logics of Pointed Latticeordered Varieties.
Logica Universalis, 2(2):209233, 2008.
(pdf,
SpringerLink)

M. Spinks and R. Veroff.
Slaney's Logic F** is Constructive Logic with Strong Negation.
Bulletin of the Section of Logic, 39(34):161174, 2010.
(Web support)

R. Padmanabhan and R. Veroff.
A Geometric Procedure with Prover9.
In M. P. Bonacina and M. Stickel (eds.),
Automated Reasoning and Mathematics: Essays in Memory of William W. McCune,
Lecture Notes in Artificial Intelligence, 7788:139150, Springer, 2013.
(Web support,
SpringerLink)

M. Kinyon, R. Veroff and P. Vojtechovsky.
Loops with Abelian Inner Mapping Groups: an Application of Automated Deduction.
In M. P. Bonacina and M. Stickel (eds.),
Automated Reasoning and Mathematics: Essays in Memory of William W. McCune,
Lecture Notes in Artificial Intelligence, 7788:151164, Springer, 2013.
(Web support,
SpringerLink)

M. Spinks, R. Bignall and R. Veroff.
Discriminator Logics (Research Announcement).
Australasian Journal of Logic, 11(2):159171, 2014.
(pdf)

J. Urban and R. Veroff.
Experiments with Stateoftheart Provers on Problems in Tarskian Geometry
In B. Konev, S. Schulz and L. Simon (eds.),
11th International Workshop on the Implementation of Logics (IWIL2015),
EPiC Series in Computing, 40:122126, EasyChair, 2016.
(EasyChair)

S. Holub and R. Veroff.
Formalizing a Fragment of Combinatorics on Words.
In J. Kari, F. Manea and I. Petre (eds.),
Computability in Europe (CiE 2017), Unveiling Dynamics and Complexity,
Lecture Notes in Computer Science, 10307:2431, Springer, 2017.
(Web support,
SpringerLink)

M. Spinks and R. Veroff.
Paraconsistent Constructive Logic with Strong Negation is a
Contractionfree Relevant Logic.
In J. Czelakowski (ed.),
Don Pigozzi on Abstract Algebra Logic, Universal Algebra, and Computer
Science, Outstanding Contributions to Logic, 16:323379, Springer, 2018.
(Springer)

R. Veroff.
A Wos Challenge Met.
Journal of Automated Reasoning, to appear.
(Web support,
Springer Link)
Last Modified: April 15, 2022 by veroff@cs.unm.edu