Interests

Logic and its applications in Computer Science: Non-Classical Logics, Proof Complexity, Type Theory, Programming Language Semantics, Automated Deduction, and Formal Verification

Education

• Ph.D., Cornell University, 1998
• Honors Diploma, Moscow State University, 1992

Journal Articles

• P. Naumov, On meta complexity of propositional formulas and propositional proofs, Archive for Mathematical Logic, pp. 35-52, v. 47, n. 1, 2008 (link)
• P. Naumov, Logic of Subtyping, Theoretical Computer Science, pp. 167-185, v. 357, n.1-3, 2006 (link)
• P. Naumov, Upper bounds on complexity of Frege proofs with limited use of certain schemata, Archive for Mathematical Logic, pp. 432-446, v. 45, 2006 (link)
• P. Naumov, On Modal Logic of Deductive Closure, Annals of Pure and Applied Logic, pp. 218-224, v. 141, n.1-2, 2006 (link)
• P. Naumov, On Modal Logics of Partial Recursive Functions, Studia Logica, pp. 295-309, v. 81, 2005, (link)
• P. Naumov, Undecidability of Second Order Provability Logic with Witness Comparison, Vestnik MGU, pp. 14-17, Vol. 48, No. 3, 1993 (Russian). English translation in Moscow University Mathematics Bulletin, Allerton Press, NY
• P. Naumov, Undecidability of Gödel-Löb Logic with Quantifiers over Propositional Variables, Vestnik MGU, pp. 13-16, Vol. 48, No. 2, 1993, (Russian). English translation in Moscow University Mathematics Bulletin, Allerton Press, NY
• P. Naumov, On Modal Logics, Conservative over Intuitionistic Calculus, Vestnik MGU, pp. 58-61, Vol. 46, No. 6, 1991 (Russian). English translation in Moscow University Mathematics Bulletin, Allerton Press, NY

Book Chapter

• R. Constable, P. Jackson, P. Naumov, and J. Uribe, Constructively Formalizing Automata Theory, in Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000

Conference Papers

• S. Miner More and P. Naumov, On Interdependence of Secrets in Collaboration Networks, Twelfth conference on Theoretical Aspects of Rationality and Knowledge (TARK '09), July 6-8, 2009, Stanford University
• S. Miner More and P. Naumov, An Independence Relation for Sets of Secrets, 16th Workshop on Logic, Language, Information and Computation (WoLLIC '09), Tokyo, Japan, June 21-24, 2009, Lecture Notes in Computer Science n.5514, Springer, 2009
• P. Naumov, On Modal Logic of Deductive Closure, Logic Colloquium 2004, ASL European Summer Meeting, Turin, Italy, July 2004, The Bulletin of Symbolic Logic, v. 11, n. 2, pp. 288-289, 2005
• P. Naumov, On Modal Logics of Computable Functions, Annual Meeting of the Association for Symbolic Logic, Pittsburgh, May 2004, The Bulletin of Symbolic Logic, v. 11, n. 1, p. 113, 2005
• P. Naumov, Logic of Subtyping, presented at The 18th Annual IEEE Symposium on Logic in Computer Science (LICS`03), Ottawa, Canada, June 2003
• P. Naumov, An extension of the classical propositional logic by type constructors, Winter Meeting of the Association for Symbolic Logic, Baltimore, January 2003, The Bulletin of Symbolic Logic, v. 9, n.2, pp. 254-255, 2003
• P. Naumov, M.-O. Stehr, and J. Meseguer, The HOL/NuPRL Proof Translator: A Practical Approach to Formal Interoperatability, The 14th International Conference on Theorem Proving in Higher Order Logics, pp. 329-345, Edinburgh, Scotland, September 2001, Lecture Notes in Computer Science, Springer
• M.-O. Stehr, P. Naumov, and J. Meseguer, A Proof-Theoretic Approach to HOL-Nuprl Connection with Applications to Proof Translation, The 15th International Workshop on Algebraic Development Techniques/General Workshop of the Common Framework Initiative, Genova, Italy, April 2001
• P. Naumov, Formalization of Isabelle Meta Logic in NuPRL, Supplemental proceedings of The 13th International Conference on Theorem Proving in Higher Order Logics,, Portland, Oregon, 2000
• P. Naumov, Importing Isabelle Formal Mathematics into NuPRL, Theorem Proving in Higher Order Logics: Emerging Trends 1999, Supplemental proceedings of The 12th International Conference on Theorem Proving in Higher Order Logics, Nice, France, 1999

Technical Reports

• P. Naumov, Theory of Reference Types, Cornell CS Technical Report 98-1711, 1998
• P. Naumov, Publishing Formal Mathematics on the Web, Cornell CS Technical Report 98-1689, 1998
• P. Naumov, Formalizing Reference Types in NuPRL, Ph.D. Dissertation, Cornell Computer Science Technical Report TR98-1709, 1998
• P. Naumov, Second Order Modal Logics with Provability Interpretation, Diploma Thesis, Moscow State University, June 1992

Teaching at McDaniel

Calculus II, College Algebra and Trigonometry, The Art of Programming, Discrete Mathematics, First Year Seminar, Numerical Methods, Data Structures, Artificial Intellegence, Graphics, Algorithms, Formal Methods, Senior Project

Previously Taught

Discrete Mathematics, Discrete Mathematical Structures, Data Structures and Algorithms, Foundations of Mathematics, Formal Languages with Applications, Software Engineering and Design, Artificial Intelligence, Object-Oriented Programming with Java, Fundamentals of Computer Science III, Formal Methods for Software Engineering, Advanced Programming Languages, Advanced Artificial Intelligence

Not to be taken too seriously ...

Advisor genealogy