Robert Veroff Professor Emeritus Computer Science Department School of Engineering University of New Mexico Affiliated Research Professor Department of Artificial Intelligence Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) Czech Technical University in Prague (CTU) Email: veroff@cs.unm.edu

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 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 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

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

miscellaneous

• Automated deduction at Argonne National Laboratory
• AI4Reason Project at the Czech Technical University
• TPTP problem library
• Mathematical Structures
• Sentential Calculi
• The QED project

Personal

• veroff.org

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 support)

• 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, Web support)

• 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, 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: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 support, SpringerLink)

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

• F. Paoli, M. Spinks and R. Veroff. Abelian Logic and the Logics of Pointed Lattice-ordered Varieties. Logica Universalis, 2(2):209-233, 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(3-4):161-174, 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:139-150, 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:151-164, Springer, 2013. (Web support, SpringerLink)

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

• J. Urban and R. Veroff. Experiments with State-of-the-art Provers on Problems in Tarskian Geometry In B. Konev, S. Schulz and L. Simon (eds.), 11th International Workshop on the Implementation of Logics (IWIL-2015), EPiC Series in Computing, 40:122-126, 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:24-31, Springer, 2017. (Web support, SpringerLink)

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

• R. Veroff. A Wos Challenge Met. Journal of Automated Reasoning, 66(4):565-574, 2022. (Web support, Springer Link)