Robert Veroff Professor Computer Science Department School of Engineering University of New Mexico Farris Engineering Center Albuquerque, NM 87131 Email: veroff@cs.unm.edu

Ph.D., Northwestern University, 1980
Primary Research Interest: automated deduction

Some Links for Automated Deduction

current

• ADAM 2008 workshop
• Basarab's Theorem in loop theory
• CD-derivation of the long Rezus single axiom for RI from {B,C,I,W}

recent applications

• Challenge problems with condensed detachment (updated December 3, 2007)
• Median algebra (updated September 28, 2006)
• A first-order 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 Boolean algebra (updated June 13, 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
• ADAM, Automated Deduction and its Application to Mathematics (workshop)

provers

• Otter, a program that searches for proofs (previous site)
• Prover9, Otter's successor

miscellaneous

• Automated deduction at Argonne National Laboratory
• Other theorem proving systems and groups and more
• Mechanized reasoning Web site at Stanford
• The QED project
• TPTP problem library

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 (Modula-2 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), Addison-Wesley, 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(1-3):175-194, 2001. (postscript)

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

• R. Veroff, Solving Open Questions and Other Challenge Problems Using Proof Sketches, Journal of Automated Reasoning, 27(2):157-174, 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):1-16, 2002. (pdf)

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

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

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

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

• W. McCune, R. Padmanabhan, M. A. Rose and R. Veroff, Short Equational Bases for Ortholattices, Tech. Report TR-CS-2004-01, 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 TR-CS-2004-02, 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):581-615, 2004. (pdf)

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

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

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

• R. Padmanabhan, W. McCune and R. Veroff. Levi's Commutator Theorems for Cancellative Semigroups. Semigroup Forum, 71:152-157, 2005. (pdf)

• M. Spinks and R. Veroff. On the Equational Definability of Brouwer-Zadeh Lattices. Tech. Report TR-CS-2006-12, 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):3-20, 2006. (pdf, errata)

• R. Padmanabhan, W. McCune and R. Veroff. Lattice Laws Forcing Distributivity Under Unique Complementation. Houston Journal of Mathematics, 33(2):391-401, 2007. (pdf)

• 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:1539-1552, 2007.

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

• M. Spinks and R. Veroff. Constructive Logic with Strong Negation is a Substructural Logic, I. Studia Logica, 88(3):325-348, 2008. (Web page, SpringerLink)

• M. Spinks and R. Veroff. Constructive Logic with Strong Negation is a Substructural Logic, II. Studia Logica, to appear.

• F. Paoli, M. Spinks and R. Veroff. Abelian logic and the logics of pointed lattice-ordered varieties. Submitted. (pdf)