|

P A V E L
N A U M O V
Assistant Professor of Computer Science,
McDaniel College
I n t e r e s t s
Logic and its applications in Computer Science: Non-Classical Logics,
Proof Complexity, Type Theory, Programming Language Semantics,
Automated Deduction, and Formal Verification
E d u c a t i o n
- Ph.D., Cornell University, 1998
- Honors Diploma, Moscow State University, 1992
T e a c h i n g @ M c D a n i e l
- CSC 1106 The Art of Programming: Spring 06, Fall 05
- CSC/MAT 1109 Discrete Mathematics: Fall 06, Spring 06
- CSC 1110 Recursion in Algorithms, Logic, and Mathematics: Fall 07, Fall 06
- CSC 2209 Computer Organization: Spring 07
- CSC/MAT 2210 Numerical Methods: Spring 07, Fall 05
- CSC 2217 Data Structures: Fall 07, Fall 06
- CSC 2265 Artificial Intellegence: Fall 05
- CSC 3315 Principles of Computer Graphics: Fall 07
- CSC 3317 Algorithms: Spring 07, Spring 06
P r e v i o u s l y T a u g h t
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
J o u r n a l A r t i c l e s
- P. Naumov,
On meta complexity of propositional formulas and propositional proofs,
Archive for Mathematical Logic, (to appear)
- 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
B o o k C h a p t e r
- 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
C o n f e r e n c e P a p e r s
- 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
T e c h n i c a l R e p o r t s
- 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
N o t t o b e t a k e n t o o s e r i o u s l y . . .
Advisor genealogy
|