**B. Konev**, C. Lutz, F. Wolter, and M. Zakharyaschev, “Conservative Rewritability of Description Logic TBoxes,” in*IJCAI 2016, Proceedings of the 25st International Joint Conference on Artificial Intelligence*, 2016.

(full version with appendix)**B. Konev**and T. Kutsia, “Anti-Unification of Concepts in Description Logic EL,” in*Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29*, 2016.

Full version is available as a RISC-Linz technical report, http://www.risc.jku.at/publications/download/risc_5266/TR.pdf**B. Konev**and A. Lisitsa, “Computer-aided proof of Erdős discrepancy properties,”*Artif. Intell.*, vol. 224, pp. 103–118, 2015.

**B. Konev**, C. Lutz, F. Wolter, and M. Zakharyaschev, “Conservative Rewritability of Description Logic TBoxes: First Results,” in*Proceedings of the 28th International Workshop on Description Logics, Athens, Greece, June 7-10, 2015.*, 2015, vol. 1350.

**B. Konev**, A. Ozaki, and F. Wolter, “Exact Learning Description Logic Ontologies from Data Retrieval Examples,” in*Proceedings of the 28th International Workshop on Description Logics, Athens, Greece, June 7-10, 2015.*, 2015, vol. 1350.

- R. Williams,
**B. Konev**, and F. Coenen, “Scalable distributed collaborative tracking and mapping with Micro Aerial Vehicles,” in*2015 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2015, Hamburg, Germany, September 28 - October 2, 2015*, 2015, pp. 3092–3097.

- W. Gatens,
**B. Konev**, and F. Wolter, “Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies,” in*Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014.*, 2014, vol. 1193, pp. 181–184.

- W. Gatens,
**B. Konev**, and F. Wolter, “Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies,” in*ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014)*, 2014, vol. 263, pp. 345–350.

- M. Ludwig and
**B. Konev**, “Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference,” in*Principles of Knowledge Representation and Reasoning. Proceedings*, 2014.

**B. Konev**, C. Lutz, A. Ozaki, and F. Wolter, “Exact Learning of Lightweight Description Logic Ontologies,” in*Principles of Knowledge Representation and Reasoning. Proceedings*, 2014.

**B. Konev**and A. Lisitsa, “A SAT Attack on the Erdős Discrepancy Conjecture,” in*Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings*, 2014, vol. 8561, pp. 219–226.

A revised extended version is available at http://arxiv.org/abs/1405.3097 See also http://cgi.csc.liv.ac.uk/%7Ekonev/edp/**B. Konev**, C. Lutz, D. Walther, and F. Wolter, “Model-theoretic inseparability and modularity of description logic ontologies,”*Artif. Intell.*, vol. 203, pp. 66–103, 2013.

- R. Williams and
**B. Konev**, “Propositional Temporal Proving with Reductions to a SAT Problem,” in*Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings*, 2013, vol. 7898, pp. 421–435.

- W. Gatens,
**B. Konev**, and F. Wolter, “Module Extraction for Acyclic Ontologies,” in*Proceedings of the 7th International Workshop on Modular Ontologies co-located with the 12th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2013), Corunna, Spain, September 15, 2013*, 2013, vol. 1081.

- C. Dixon,
**B. Konev**, M. Fisher, and S. Nietiadi, “Deductive temporal reasoning with constraints,”*Journal of Applied Logic*, vol. 11, no. 1, pp. 30–51, 2013.

**B. Konev**, C. Lutz, and F. Wolter, “Exact Learning of TBoxes in EL and DL-Lite,” in*Informal Proceedings of the 26th International Workshop on Description Logics, Ulm, Germany, July 23 - 26, 2013*, 2013, vol. 1014, pp. 341–352.

- M. Ludwig and
**B. Konev**, “Towards Practical Uniform Interpolation and Forgetting for ALC TBoxes,” in*Informal Proceedings of the 26th International Workshop on Description Logics, Ulm, Germany, July 23 - 26, 2013*, 2013, vol. 1014, pp. 377–389.

**B. Konev**, M. Ludwig, D. Walther, and F. Wolter, “The Logical Difference for the Lightweight Description Logic EL,”*Journal of Artificial Intelligence Research (JAIR)*, vol. 44, pp. 633–708, 2012.

**B. Konev**, M. Ludwig, and F. Wolter, “Logical Difference Computation with CEX2.5,” in*Proceedings International Joint Conference on Automated Reasoning*, 2012, pp. 371–377.

- A. Niknafs-Kermani,
**B. Konev**, and M. Fisher, “Symmetric Temporal Theorem Proving,” in*TIME*, 2012, pp. 21–28.

**B. Konev**, R. Kontchakov, M. Ludwig, T. Schneider, F. Wolter, and M. Zakharyaschev, “Conjunctive Query Inseparability of OWL 2 QL TBoxes,” in*Proceedings of the Twenty-Fifth AAAI conference on Artificial Intelligence*, 2011.

**B. Konev**, C. Lutz, D. Ponomaryov, and F. Wolter, “Decomposing Description Logic Ontologies,” in*Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010, Toronto, Ontario, Canada, May 9-13, 2010*, 2010.

**B. Konev**, D. Walther, and F. Wolter, “Forgetting and Uniform Interpolation in Extensions of the Description Logic EL,” in*Description Logics Workshop*, 2009, vol. 477.

- C. Dixon, M. Fisher, and
**B. Konev**, “Taming the Complexity of Temporal Epistemic Reasoning,” in*Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009*, 2009, vol. 5749, pp. 198–213.

**B. Konev**, C. Lutz, D. Walther, and F. Wolter, “Formal Properties of Modularisation,” in*Modular Ontologies*, vol. 5445, Springer, 2009, pp. 25–66.

- M. Fisher,
**B. Konev**, and A. Lisitsa, “Temporal Verification of Fault-Tolerant Protocols,” in*Methods, Models and Tools for Fault Tolerance*, vol. 5454, Springer, 2009, pp. 44–56.

**B. Konev**, D. Walther, and F. Wolter, “Forgetting and Uniform Interpolation in Large-Scale Description Logic Terminologies,” in*IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence*, 2009, pp. 830–835.

**B. Konev**, R. A. Schmidt, and S. Schulz, Eds.,*Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning*, vol. 373. CEUR-WS.org, 2008.

- P. Rudnicki, G. Sutcliffe,
**B. Konev**, R. Schmidt, and S. Schulz, Eds.,*Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics*, vol. 418. CEUR-WS.org, 2008.

**B. Konev**, C. Lutz, D. Walther, and F. Wolter, “Logical Difference and Module Extraction with CEX and MEX,” in*Description Logics Workshop*, 2008, vol. 353.

- C. Dixon, M. Fisher,
**B. Konev**, and A. Lisitsa, “Practical First-Order Temporal Reasoning,” in*15th International Symposium on Temporal Representation and Reasoning, TIME 2008*, 2008, pp. 156–163.

**B. Konev**, D. Walther, and F. Wolter, “The Logical Difference Problem for Description Logic Terminologies,” in*Automated Reasoning, 4th International Joint Conference*, 2008, vol. 5195, pp. 259–274.

**B. Konev**, C. Lutz, D. Walther, and F. Wolter, “Semantic Modularity and Module Extraction in Description Logics,” in*ECAI 2008 - 18th European Conference on Artificial Intelligence*, 2008, vol. 178, pp. 55–59.

**B. Konev**and F. Wolter, Eds.,*Proceedings of 6th International Symposium on Frontiers of Combining Systems (FroCoS 2007)*, vol. 4720. 2007.

- C. Dixon, M. Fisher, and
**B. Konev**, “Temporal Logic with Capacity Constraints,” in*Proceedings of 6th International Symposium on Frontiers of Combining Systems (FroCoS 2007)*, 2007, pp. 163–177.

- C. Dixon, M. Fisher, and
**B. Konev**, “Tractable Temporal Reasoning,” in*Proceedings 20 International Joint Conference on Artificial Intelligence*, 2007, pp. 318–323.

- M. Fisher, W. van der Hoek,
**B. Konev**, and A. Lisitsa, Eds.,*Logics in Artificial Intelligence, 10th European Conference, JELIA 2006*. 2006.

**B. Konev**, R. Kontchakov, F. Wolter, and M. Zakharyaschev, “Dynamic topological logics over spaces with continuous functions,” in*Proceedings of Advances in Modal Logic 2006 (AiML)*, 2006.

- A. Degtyarev, M. Fisher, and
**B. Konev**, “Monodic Temporal Resolution,”*ACM Transactions on Computational Logic*, vol. 7, no. 1, 2006.

- C. Dixon, M. Fisher, and
**B. Konev**, “Is there a future for deductive temporal verification?,” in*Proceedings of International Symposium on Temporal Representation and Reasoning (TIME)*, 2006, pp. 11–18.

- A. Lyaletski and
**B. Konev**, “On Herbrand’s theorem for intuitionistic logic,” in*Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA’06)*, 2006.

**B. Konev**, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt, “Mechanising first-order temporal resolution,”*Information and Computation*, vol. 199, no. 1–2, pp. 55–86, 2005.

- U. Hustadt,
**B. Konev**, and R. A. Schmidt, “Deciding Monodic Fragments by Temporal Resolution,” in*Proceedings of the 20th International Conference on Automated Deduction CADE-20 (Tallinn, Estonia, July 22-27, 2005)*, 2005, vol. 3632, pp. 204–218.

**B. Konev**, F. Wolter, and M. Zakharyaschev, “Temporal Logics over Transitive States,” in*Proceedings of the 20th International Conference on Automated Deduction CADE-20 (Tallinn, Estonia, July 22-27, 2005)*, 2005, vol. 3632, pp. 182–203.

[ pdf ] [ abstract ]We investigate the computational behaviour of ‘two-dimen\-sional’ propositional temporal logics over (\nat ,<) (with and without the next-time operator \nxt) that are capable of reasoning about states with transitive relations. Such logics are known to be undecidable (even \Pi^1_1-complete) if the domains of states with those relations are assumed to be constant. Motivated by applications in the areas of temporal description logic and specification & verification of hybrid systems, in this paper we analyse the computational impact of allowing the domains of states to expand. We show that over finite expanding domains (with an arbitrary, tree-like, quasi-order, or linear transitive relation) the logics are recursively enumerable, but undecidable. If these finite domains eventually become constant then the resulting \nxt-free logics are decidable (but not in primitive recursive time); on the other hand, when equipped with \nxt they are not even recursively enumerable. Finally, we show that temporal logics over infinite expanding domains as above are undecidable even for the language with the sole temporal operator ‘eventually.’ The proofs are based on Kruskal’s tree theorem and reductions of reachability problems for lossy channel systems. ×

- U. Hustadt and
**B. Konev**, “TRP++: A Temporal Resolution Prover,” in*Collegium Logicum*, vol. 8, KGS Wien, 2004.

**B. Konev**, R. Kontchakov, F. Wolter, and M. Zakharyaschev, “On dynamic topological and metric logics,” in*Proceedings of AiML 04*, 2004.

- U. Hustadt,
**B. Konev**, A. Riazanov, and A. Voronkov, “\textbfTeMP: A Temporal Monodic Prover,” in*Proceedings International Joint Conference on Automated Reasoning*, 2004, vol. 3097, pp. 326–330.

**B. Konev**, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt, “Towards the implementation of first-order temporal resolution: the expanding domain case,” in*Proceedings TIME-ICTL’03*, 2003, pp. 72–82.

- A. Degtyarev, M. Fisher, and
**B. Konev**, “Monodic temporal resolution,” in*Proceedings of the 19th International Conference on Automated Deduction, CADE-19*, 2003, vol. 2741, pp. 397–411.

- U. Hustadt and
**B. Konev**, “TRP++ 2.0: A temporal resolution prover,” in*Proceedings of the 19th International Conference on Automated Deduction, CADE-19*, 2003, vol. 2741, pp. 274–278.

- A. Degtyarev, M. Fisher, and
**B. Konev**, “Handling equality in monodic temporal resolution,” in*Proceedings of 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)*, Almaty, Kazakhstan, 2003, vol. 2850, pp. 214–228.

- U. Hustadt and
**B. Konev**, “TRP++: A temporal resolution prover,” in*Proceedings of 3d International Workshop on the Implementation of Logics*, 2002.

- A. Degtyarev, M. Fisher, and
**B. Konev**, “A simplified clausal resolution procedure for propositional linear-time temporal logic,” in*Tableaux 2002, Proceedings*, 2002, vol. 2381, pp. 85–99.

**B. Konev**and T. Jebelean, “Solution lifting method for handling Meta-variables in the THEOREMA system,”*Zapiski Nauchnykh Seminarov POMI*, vol. 293, pp. 94–117, 2002.

English translation: \em Journal of Mathematical Sciences, Plenum/Kluwer.- E. Dantsin, E. A. Hirsch, M. Gavrilovich, and
**B. Konev**, “MAXSAT Approximation Beyond the Limits of Polynomial-Time Approximation,”*Annals of Pure and Applied Logic*, vol. 113, no. 1–3, pp. 81–94, 2001.

**B. Konev**, “Upper bound on the height of terms in proofs with bound-depth-restricted cuts,”*Zapiski Nauchnykh Seminarov POMI*, vol. 277, pp. 80–103, 2001.

English translation: \em Journal of Mathematical Sciences, Plenum/Kluwer.

**B. Konev**and T. Jebelean, “Solution Lifting Method for Handling Meta-Variables in Theorema,”*Annals of the University of Timisoara*, vol. XXXIX, pp. 81–106, 2001.

**B. Konev**, “Refinement of bounds of the height of terms in the most general unifier,”*Journal of Mathematical Sciences*, vol. 98, p. 4, 2000.

**B. Konev**and T. Jebelean, “Using Meta-Variables for Natural Deduction in THEOREMA,” in*Calculemus 2000: integration of symbolic computation and mechanized reasoning*, A. K. Peters, Natik, Massatchussets, 2000.

**B. Konev**, “Upper bound on the height of terms in proofs with cuts,” Steklov Institute of Mathematics at St.Petersburg , 17/1998, Aug. 1998.

**B. Konev**, “Upper bound on the height of terms in proofs with cuts,” in*Proceedings of First-order Theorem Proving—FTP’98 / 2nd International Workshop on First-order Theorem Proving, Vienna, Austria*, 1998, pp. 162–172.

Professor
Boris Konev

Department of Computer Science

University of Liverpool

Ashton Building

Liverpool
L69 3BX,
UK

**Tel:**
+44 (0)151 795 4260

**Email:**
konev@liverpool.ac.uk

**Office:** Room 1.15 (Ashton building)