Publications


Publications in reverse chronological order | Publications ordered by theme | Current DBLP listing | Scholar Google | Arnetminer | Academic Search
To appear | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 - 2005 | 2004 - 2000 | 1999 - 1995 | 1994 - 1991

To appear
Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Kambhampati, S. (ed), Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016). AAAI Press.
Abstract, BiBTeX.
Lifting QBF Resolution Calculi to DQBF. Together with O. Beyersdorff, L. Chew and M. Suda. In Creignou, N. and Le Berre, D. (eds), Theory and Applications of Satisfiability Testing (SAT 2016). Lecture Notes in Computer Science, Vol. ????, Springer, ??-??.
Abstract, BiBTeX, ECCC Report.
A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming ?? (??) ??-??. To appear.
Abstract, BiBTeX, Accepted online version at Elsevier via DOI Link.
2016
Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Lenzerini, M. and Penaloza, R. (eds), Proceedings of the 29th International Workshop on Description Logics (DL-2016). CEUR Workshop Proceedings, Vol. 1577, CEUR-WS.org.
Abstract, BiBTeX, PDF.
2015
Modal Tableau Systems with Blocking and Congruence Closure. Together with U. Waldmann. In De Nivelle, H. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015). Lecture Notes in Computer Science, Vol. 9323, Springer, 38-53.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Arenas et al (eds), The Semantic Web, 14th International Semantic Web Conference, ISWC 2015. Lecture Notes in Computer Science, Vol. 9366, Springer, 587-602.
Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Together with P. Koopmann. In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach. Together with Y. Zhao. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Saturation-Based Forgetting in the Description Logic SIF. Together with P. Koopmann. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. Together with P. Koopmann. In Bonet, B. and Koenig, S. (eds), Proc. AAAI-2015. AAAI Press, 175-181.
Abstract, BiBTeX, PDF.
2014
Axiomatic and Tableau-Based Reasoning for Kt(H,R). Together with J. G. Stell and D. Rydeheard. In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497,
Abstract, BiBTeX, PDF (final version available in the proceedings).
Forgetting and Uniform Interpolation of ALC-Ontologies with ABoxes. Together with P. Koopmann. In M. Bienvenu and R. Rosati (eds), Proceedings of the 27th International Workshop on Description Logics (DL-2014). CEUR Workshop Proceedings, Vol. 1193, CEUR-WS.org, 245-257.
Abstract, BiBTeX, PDF.
Terminating Minimal Model Generation Procedures for Propositional Modal Logics. Together with F. Papacchini. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 381-395.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Count and Forget: Uniform Interpolation of SHQ-Ontologies. Together with P. Koopmann. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 434-448.
Abstract, BiBTeX, Long version (final version available via DOI link to Springer).
Tableau Development for a Bi-Intuitionistic Tense Logic. Together with J. G. Stell and D. Rydeheard. In Hofner, P., Jipsen, P., Kahl, W. and Müller, M. E. (eds), Relational and Algebraic Methods in Computer Science (RAMiCS 14). Lecture Notes in Computer Science, Vol. 8428, Springer, 412-428.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. ACM Transactions on Computational Logic 15 (1).
Abstract, BiBTeX, PDF (DOI link to TOCL).
2013
Forgetting Concept and Role Symbols in ALCH-Ontologies. Together with P. Koopmann. In McMillan, K., Middeldorp, A. and Voronkov, A. (eds), Proc. LPAR 2013. Lecture Notes in Computer Science, Vol. 8312, Springer, 552-567.
Abstract, BiBTeX, PDF (final version will be available from Springer).
Implementation and Evaluation of Forgetting in ALC-Ontologies. Together with P. Koopmann. In Del Vescovo, C., Hahmann, T., Pearce, D. and Walther, D. (eds), Proceedings of the 7th International Workshop on Modular Ontologies (WoMo 2013). CEUR Workshop Proceedings, Vol. 1081, CEUR-WS.org, 1-12.
Abstract, BiBTeX, PDF, Electronic edition at CEUR-WS.org.
Frontiers of Combining Systems-FroCoS 2013. 9th International Symposium on Frontiers of Combining Systems, Nancy, September 18-20, 2013. Proceedings. Together with P. Fontaine and C. Ringeissen (eds). Lecture Notes in Artificial Intelligence, Vol. 8152, Springer.
Abstract, BiBTeX, DOI Link.
Uniform Interpolation of ALC-Ontologies Using Fixpoints. Together with P. Koopmann. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 87-102.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Computing Minimal Models Modulo Subset-Simulation for Propositional Modal Logics. Together with F. Papacchini. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 279-294.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. Together with M. Khodadadi and D. Tishkovsky. In Galmiche, D. and Larchey-Wendling, D. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013). Lecture Notes in Computer Science, Vol. 8123 Springer, 188-202.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics. Together with S. Minica, M. Khodadadi and D. Tishkovsky. In Fontaine, P. and Schmidt, R. A. and Schulz, S. (eds), PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 21 EasyChair, 109-123.
Abstract, BiBTeX, Link to EasyChair Proceedings.
MetTeL2: Towards a Tableau Prover Generation Platform. Together with D. Tishkovsky and M. Khodadadi. In Fontaine, P. and Schmidt, R. A. and Schulz, S. (eds), PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 21 EasyChair, 149-162.
Abstract, BiBTeX, PDF, Link to EasyChair Proceedings.
PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. Together with P. Fontaine and S. Schulz (eds). EPiC Series, Vol. 21, EasyChair.
Abstract, BiBTeX, Proceedings.
Refinement in the Tableau Synthesis Framework. Together with D. Tishkovsky. arXiv e-Print 1305.3131v1 [cs.LO].
Abstract, BiBTeX, arXiv Link.
First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science Vol. 7797, 345-391. Springer. Invited overview paper.
Abstract, BiBTeX, DOI.
Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete. Together with M. Zawidzki and D. Tishkovsky. Information Processing Letters 113 (1-2) 34-38.
Abstract, BiBTeX, DOI.
2012
Labelled Tableaux for Temporal Logic with Cardinality Constraints. Together with C. Dixon, B. Konev, and D. Tishkovsky. Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012). IEEE Computer Society, 111-118.
Abstract, BiBTeX, DOI, PDF.
The Tableau Prover Generator MetTeL2. Together with D. Tishkovsky and M. Khodadadi. In del Cerro, L. F. and Herzig, A. and Mengin, J. (eds), Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA 2012). Lecture Notes in Computer Science Vol. 7519, Springer, 492-495.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. arXiv e-Print 1208.1476v1 [cs.LO].
Abstract, BiBTeX, arXiv Link.
An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting. Together with M. Khodadadi and D. Tishkovsky. In Kazakov, Y. and Lembo, D. and Wolter, F. (eds), Proceedings of the 2012 International Workshop on Description Logics (DL-2012)., CEUR Workshop Proceedings 846, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Proceedings of the 19th Automated Reasoning Workshop. Together with F. Papacchini (eds). Escholar uk-ac-man-scw:161817, The University of Manchester, UK.
Abstract, BiBTeX, Proceedings.
PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. Together with B. Konev and S. Schulz (eds). EPiC Series, Vol. 9, EasyChair.
Abstract, BiBTeX, Proceedings.
A Comparison of Solvers for Propositional Dynamic Logic. Together with U. Hustadt. In Konev, B. and Schmidt, R. and Schulz, S. (eds), PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 9, EasyChair, 63-73.
Abstract, BiBTeX, PDF.
The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction. Journal of Applied Logic 10 (1) 52-74.
Abstract, BiBTeX, DOI.
2011
A Tableau Calculus for Minimal Modal Model Generation. Together with F. Papacchini. Electronic Notes in Theoretical Computer Science 278 (3), 159-172.
Abstract, BiBTeX, DOI Link.
Special Issue of Selected Extended Papers of CADE-22. Together with Brigitte Pientka (eds). Journal of Automated Reasoning 47 (2) (2011).
BiBTeX, Editorial, Special issue.
MetTeL: A Tableau Prover with Logic-Independent Inference Engine. Together with D. Tishkovsky and M. Khodadadi. In Brunnler, K. and Metcalfe, G. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011). Lecture Notes in Artificial Intelligence, Vol. 6793, Springer, 242-247.
Abstract, BiBTeX, DOI Link.
Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. Logical Methods in Computer Science 7 (2) 1-32,
Abstract, BiBTeX, Link to journal, arXiv Link.
Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper. In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49.
Abstract, BiBTeX, DOI Link.
2010
Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262, 221-229. Invited paper.
Abstract, BiBTeX, PDF, DOI Link.
A Tableau Method for Checking Rule Admissibility in S4. Together with S. Babenyshev, V. Rybakov and D. Tishkovsky. Electronic Notes in Theoretical Computer Science 262 17-32.
Abstract, BiBTeX, PDF, DOI Link.
Special issue on Practical Aspects of Automated Reasoning. Together with B. Konev and S. Schulz (eds). AI Communications 23 (2-3) 67-68.
BiBTeX, Editorial, Special issue.
2009
Reasoning Web: Semantic Technologies for Information Systems. 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30-September 4, 2009, Tutorial Lectures. Together with Tessaris, S., Franconi, E., Eiter, Th., Gutierrez, C., Handschuh, S., Rousset, M.-C. (eds), Lecture Notes in Computer Science: Information Systems and Applications, incl. Internet/Web, and HCI, Vol. 5689, Springer.
Abstract, BiBTeX, DOI Link.
Automated Deduction-CADE-22. 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Schmidt, R. A. (ed), Lecture Notes in Artificial Intelligence, Vol. 5663, Springer.
Abstract, BiBTeX, DOI Link.
Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324.
Abstract, BiBTeX, PDF, DOI Link.
A New Methodology for Developing Deduction Methods. In Annals of Mathematics and Artificial Intelligence 55 (1-2) 155-187.
Abstract, BiBTeX, PDF, DOI Link.
Special issue on Empirically Successful Computerized Reasoning. Together with G. Sutcliffe and S. Schulz (eds). Journal of Applied Logic 7 (1).
Abstract, BiBTeX, Link to JAL.
2008
Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics (KEAPPA & IWIL 2008). Together with Rudnicki, P., Sutcliffe, G., Konev, B., and Schulz, S. (eds), CEUR Workshop Proceedings, Vol. 418.
Abstract, BiBTeX, Full text via CEUR.
Improved Second-Order Quantifier Elimination in Modal Logic. In Hölldobler, S., Lutz, C. and Wansing, H. (eds), Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Computer Science, Vol. 5293, Springer, 375-388.
Abstract, BiBTeX, DOI Link.
Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning (PAAR-2008/ESHOL-2008). Together with B. Konev and S. Schulz (eds). CEUR Workshop Proceedings, Vol. 373.
Abstract, BiBTeX, Full text via CEUR.
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. Together with D. Tishkovsky. In Armando, A., Baumgartner, P. and Dowek, G. (eds), Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science, Vol. 5195, Springer, 194-209.
Abstract, BiBTeX, DOI Link.
Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications.
Back-cover, BiBTeX, Publisher's info.
Order at amazon.co.uk, Order at amazon.com, Order at amazon.de.
Special issue on Relations and Kleene Algebras in Computer Science. Together with G. Struth (eds). Journal of Logic and Algebraic Programming 76 (1).
Abstract, BiBTeX, Link to JLAP.
On Combinations of Propositional Dynamic Logic and Doxastic Modal Logics. Together with D. Tishkovsky. Journal of Logic, Language and Information 17 (1) 109-129.
Abstract, BiBTeX, Full text via Springer.
2007
Using Tableau to Decide Expressive Description Logics with Role Negation. Together with D. Tishkovsky. In Aberer, K. et al (eds), The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007. Lecture Notes in Computer Science, Vol. 4825, Springer, 438-451.
Abstract, BiBTeX, DOI Link.
The Axiomatic Translation Principle for Modal Logic. Together with U. Hustadt. ACM Transactions on Computational Logic 8 (4) 1-55.
Abstract, BiBTeX, PDF, Final version at Elsevier via DOI Link.
System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520.
Abstract, BiBTeX, DOI Link.
Deciding ALBO with Tableau. Together with D. Tishkovsky. In Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., and Turhan, A. Y. (eds), Proceedings of the 20th International Workshop on Description Logics (DL-2007), Bozen-Bolzano University Press, 135-146.
Abstract, BiBTeX, PDF.
Computational Modal Logic. Together with I. Horrocks, U. Hustadt, and U. Sattler. In Blackburn, P. and van Benthem, J. and Wolter, F. (eds), Handbook of Modal Logic. Studies in Logic and Practical Reasoning, Volume 3, Elsevier, Amsterdam, 181-245. Commissioned overview paper.
Abstract, BiBTeX, Link to Elsevier.
2006
Investigating Finite Models of Non-Classical Logics with Relation Algebra and RelView. Together with R. Berghammer. In de Swart, H. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments II, Lecture Notes in Artficial intelligence Vol. 4342, Springer, 31-49.
Abstract, BiBTeX, PDF.
Developing Modal Tableaux and Resolution Methods via First-Order Resolution. In Governatori, G. and Hodkinson, I. and Venema, Y. (eds), Advances in Modal Logic, Volume 6. College Publications, London, 1-26. Invited paper.
Abstract, BiBTeX, PostScript.
Relations and Kleene Algebra in Computer Science: Proceedings of RelMiCS/AKA 2006. Schmidt, R. A. (ed), Lecture Notes in Computer Science, Vol. 4136, Springer.
Abstract, BiBTeX, DOI Link.
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139.
Abstract, BiBTeX, Full text via Springer.
Special issue on Implementation of Logics. Together with B. Konev and S. Schulz (eds). Journal of Applied Non-Classical Logic 16 (1-2).
Abstract, BiBTeX, Full text via JANCL.
Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), 3rd International Joint Conference on Automated Reasoning. Together with G. Sutcliffe and S. Schulz (eds). CEUR Workshop Proceedings, Vol. 192.
Abstract, BiBTeX, Full text via CEUR.
Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In C. Rouff, M. Hinchey, J. Rash, W. Truszkowski, and D. Gordon-Spears, editors, Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering Series, Springer.
Abstract, BiBTeX, PDF.
2005
Advances in Modal Logic, Volume 5. Together with I. Pratt-Hartmann, M. Reynolds, and H. Wansing (eds). King's College Publications, London.
Abstract, BiBTeX, Online version.
Deciding Monodic Fragments by Temporal Resolution. Together with U. Hustadt and B. Konev. In Nieuwenhuis, R. (eds), Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Lecture Notes in Artificial Intelligence, Vol. 3632, Springer, 204-218.
Abstract, BiBTeX, PDF, Full text via Springer.
2004
A Survey of Decidable First-Order Fragments and Description Logics. Together with U. Hustadt and L. Georgieva. Journal of Relational Methods in Computer Science 1, 251-276. Invited overview paper.
Abstract, BiBTeX, PostScript, PDF.
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. Preprint Series CSPP-22, University of Manchester, UK.
Abstract, BiBTeX, PostScript, SpringerLink.
Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. Together with D. Tishkovsky and U. Hustadt. Studia Logica 78 (3), 381-415.
Abstract, BiBTeX, SpringerLink.
AiML-2004: Advances in Modal Logic. Together with I. Pratt-Hartmann, M. Reynolds and H. Wansing (eds). Technical Report UMCS-04-09-01, University of Manchester, UK.
Abstract, BiBTeX, PDF.
Multi-Agent Dynamic Logics with Informational Test. Together with D. Tishkovsky. Annals of Mathematics and Artificial Intelligence 42 (1-3), 5-36.
Abstract, BiBTeX, SpringerLink.
SCAN is complete for all Sahlqvist formulae. Together with V. Goranko, U. Hustadt, D. Vakarelov. In Berghammer, R., Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 149-162.
Abstract, BiBTeX, PDF.
Two Proof Systems for Peirce Algebras. Together with E. Orlowska and U. Hustadt. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science, Vol. 3051, Springer, 238-251.
Abstract, BiBTeX, Springer Link.
2003
Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic Together with D. Tishkovsky and U. Hustadt. Preprint Series CSPP-27, University of Manchester, UK.
Abstract, BiBTeX, PostScript.
Mechanised Reasoning and Model Generation for Extended Modal Logics. Together with U. Hustadt. In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science Vol. 2929, Springer, 38-67. Survey commissioned for the Kickoff Volume of COST Action 274.
Abstract, BiBTeX, PDF.
Fourth International Workshop on the Implementation of Logics. Together with B. Konev (eds). Technical Report ULCS-03-018, University of Liverpool.
Abstract, BiBTeX, PDF.
Combining Dynamic Logic with Doxastic Modal Logics. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 4. Chapter 18, King's College London Publications, 371-391.
Abstract, BiBTeX.
Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation 36 (1-2), 163-192.
Abstract, ScienceDirect, BiBTeX.
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. In Baader, F. (ed.), Automated Deduction-CADE-19. Lecture Notes in Artificial Intelligence Vol. 2741, Springer, 412-426.
Abstract, BiBTeX, PostScript.
2002
Logics with Commuting Action and Informational Modalities. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. (eds), Advances in Modal Logic, Workshop Proceedings AiML'2002. 91-108.
Abstract, BiBTeX.
Multi-Agent Logic of Dynamic Belief and Knowledge. Together with D. Tishkovsky. In Flesca, S. and Greco, S. and Leone, N. and Ianni, G. (eds), Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Artificial Intelligence Vol. 2424, Springer, 38-49.
Abstract, BiBTeX, PostScript.
A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester. Long version of a paper published in Proc. CADE'2002, LNAI, Springer.
Abstract, BiBTeX, PostScript.
On the Relationship Between Decidable Fragments, Non-Classical Logics, and Description Logics. Together with L. Georgieva and U. Hustadt. In Horrocks, I. and Tessaris, S. (eds), Proceedings of the 2002 International Workshop on Description Logics (DL'2002). CEUR Workshop Proceedings, Vol. CEUR-WS/Vol-53, 25-36.
Abstract, BiBTeX, PostScript.
On Axiomatic Products of PDL and S5: Substitution, Tests and Knowledge. Together with D. Tishkovsky. Bulletin of the Section of Logic 31 (1), 27-36.
BiBTeX, PostScript.
Scientific Benchmarking with Temporal Logic Decision Procedures. Together with U. Hustadt. In Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.-A. (eds), Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR'2002). Morgan Kaufmann, 533-544.
Abstract, BiBTeX, PDF.
Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. Journal of Automated Reasoning 28 (2) 205-232.
Abstract, BiBTeX, PostScript, DOI Link.
2001
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In R. Nieuwenhuis and A. Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning (Proc. LPAR'2001). Lecture Notes in Artificial Intelligence Vol. 2250, Springer, 85-99.
Abstract, BiBTeX, DOI Link.
Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Together with U. Hustadt. In Giunchiglia, E. and Massacci, F. (eds), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Technical Report DII 14/01, Dipartimento di Ingegneria dell'Informazione, Unversitä degli Studi di Siena, Siena, Italy, 68-76.
Abstract, BiBTeX, PostScript.
Reasoning about Agents in the KARO Framework. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Bettini, C. and Montanari, A. (eds), Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME'2001). IEEE Computer Society, 206-213.
Abstract, BiBTeX.
Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Rash, J. L., Rouff, C. A., Truszkowski, W., Gordon, D. and Hinchey, M. G. (eds), Formal Approaches to Agent-Based Systems. Lecture Notes in Artificial Intelligence Vol. 1871, Springer, 33-47.
Abstract, BiBTeX.
A Resolution-Based Decision Procedure for Extensions of K4. Together with H. Ganzinger, U. Hustadt and C. Meyer. In Zakharyaschev, M. and Segerberg, K. and de Rijke, M. and Wansing, H. (eds), Advances in Modal Logic, Volume 2. Lecture Notes 119, CSLI Publications, Stanford, 225-246.
Abstract, BiBTeX, PostScript.
2000
Relational Grammars for Knowledge Representation. In Böttner, M. and Thümmel, W. (eds), Variable-Free Semantics. Artikulation und Sprache, Vol. 3, secolo Verlag, Osnabrück, Germany, 162-180.
Abstract, BiBTeX, PostScript.
MSPASS: Modal Reasoning by Translation and First-Order Resolution. Together with U. Hustadt. In Dyckhoff, R. (ed), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000). Lecture Notes in Artificial Intelligence Vol. 1847, Springer, 67-71.
Abstract, BiBTeX, PostScript.
Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In Baumgartner, P. and Zhang, H. (eds), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000). Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau, 101-112.
Abstract, BiBTeX, PostScript.
A Resolution Decision Procedure for Fluted Logic. Together with U. Hustadt. In McAllester, D. (ed), Automated Deduction-CADE-17. Lecture Notes in Artificial Intelligence Vol. 1831, Springer, 433-448.
Abstract, BiBTeX.
Resolution-Based Methods for Modal Logics. Together with H. de Nivelle and U. Hustadt. Logic Journal of the IGPL 8 (3) 265-292.
Abstract, BiBTeX, PostScript, Errata.
Normal Forms and Proofs in Combined Modal and Temporal Logics . Together with U. Hustadt, C. Dixon, and M. Fisher. In H. Kirchner and C. Ringeissen (eds), Proceedings of the International Workshop on Frontiers of Combining Systems (FroCoS'2000). Lecture Notes in Artificial Intelligence Vol. 1794, Springer, 73-87.
Abstract, BiBTeX, PostScript.
Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. In Gent, I. P. and van Maaren, H. and Walsh, T. (eds), SAT 2000: Highlights of Satisfiability Research in the Year 2000. Frontiers in Artificial Intelligence and Applications 63, IOS Press, Amsterdam. Also in a special issue of Journal of Automated Reasoning.
Abstract, BiBTeX, PostScript.
Issues of Decidability for Description Logics in the Framework of Resolution. Together with U. Hustadt. In Caferra, R. and Salzer, G. (eds), Automated Deduction in Classical and Non-Classical Logic, Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, 191-205.
Abstract, BiBTeX, PostScript.
1999
An Empirical Analysis of Modal Theorem Provers. Together with U. Hustadt. Journal of Applied Non-Classical Logics 9(4) 479-522.
Abstract, BiBTeX, PostScript.
MSPASS: Subsumption Testing with SPASS. Together with U. Hustadt and C. Weidenbach. In Lambrix, P. et al. (eds.), Proc. of Intern. Workshop on Description Logics'99, Linköping University, 136-137.
Abstract, BiBTeX, PostScript.
Decidability by Resolution for Propositional Modal Logics. Journal of Automated Reasoning 22(4), 379-396.
Abstract, BiBTeX, DOI Link.
On the Relation of Resolution and Tableaux Proof Systems for Description Logics. Together with U. Hustadt. In Dean, T. (ed), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99). Vol. 1, Morgan Kaufmann, 110-115.
Abstract, BiBTeX, PostScript.
Maslov's Class K Revisited. Together with U. Hustadt. In H. Ganzinger (ed.), Automated Deduction: CADE-16, Lecture Notes in Artificial Intelligence, Vol. 1632, Springer.
Abstract, BiBTeX, PostScript.
1998
Simplification and Backjumping in Modal Tableau. Together with U. Hustadt. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 187-201.
Abstract, BiBTeX, PostScript.
Optimised Functional Translation and Resolution. Together with U. Hustadt and C. Weidenbach. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 36-37. (Contribution to the comparison section of modal theorem provers).
Abstract, BiBTeX, PostScript.
Resolution is a Decision Procedure for Many Propositional Modal Logics. In Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 1, Lecture Notes 87, CSLI Publications, Stanford, 189-208.
Abstract, BiBTeX.
E-Unification for Subsystems of S4. In Nipkow, T. (ed.), Rewriting Techniques and Applications: 9th International Conference, RTA'98, Tsukuba, Japan, Proceedings, Lecture Notes in Computer Science Vol. 1379, Springer, 106-120.
Abstract, BiBTeX, PostScript.
Ordered E-Resolution and Path Logics. Manuscript. Submitted for publication.
Abstract, BiBTeX.
1997
Functional Translation and Second-Order Frame Properties of Modal Logics. Together with H.J. Ohlbach. Journal of Logic and Computation 7(5), 581-603.
Abstract, BiBTeX.
On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. In Pollack, M. (ed), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), Vol. 1, Morgan Kaufmann, 202-207.
Abstract, BiBTeX.
Optimised Modal Translation and Resolution. PhD Thesis, Universität des Saarlandes, Saarbrücken, Germany.
Abstract, BiBTeX, PostScript (851KB).
Decidability by resolution for many modal logics. Extended abstract of a talk presented at ESSLLI'97, Aix-en-Provence, France.
Dvi.
On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. Research Rep. MPI-I-97-2-003, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, PostScript.
Resolution is a Decision Procedure for Many Propositional Modal Logics. Research Rep. MPI-I-97-2-002, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, PostScript.
1996
Translating Graded Modalities into Predicate Logic. Together with H.J. Ohlbach and U.Hustadt. In H. Wansing (ed), Proof Theory for Modal Logic, Applied Logic Series 2, Kluwer, 253-291.
Abstract, BiBTeX.
1995
Symbolic Arithmetical Reasoning with Qualified Number Restrictions. Together with H.J. Ohlbach and U. Hustadt. In Proc. of Intern. Workshop on Description Logics'95 (held in Rome, 2-3 June 1995), Rap.07.95, Dipartimento di Informatica e Sistemistica, Univ. degli studia di Roma, 89-95.
Abstract, BiBTeX, PostScript
The Optimised Functional Translation and Graded Modal Logics. Together with H.J. Ohlbach. Combined abstract of talks held at the RelMiCs'96 Workshop in Parati, Brasil, 10-14 July.
Abstract, BiBTeX, DVI, PostScript
1994
Peirce Algebras. Together with C. Brink and K. Britz. Formal Aspects of Computing 6 (3), 339-358.
Abstract, BiBTeX, DVI, PostScript, DOI Link.
Peirce Algebras and Their Applications in Artificial Intelligence and Computational Linguistics: Abstract. SIGALA Newsletter 2 (1) 27. Abstract of a talk held at the Dagstuhl Seminar on Relational Methods in Computer Science, Dagstuhl, Germany (January 1994).
Abstract, BiBTeX, DVI, PostScript
Description Logics for Natural Language Processing. Together with D. Fehrer, U. Hustadt, M. Jaeger, A. Nonnengart, H.J. Ohlbach, Ch. Weidenbach and E. Weydert. In Proc. of Intern. Workshop on Description Logics'94, Document D-94-10, DFKI, Saarbrücken, 80-84.
Abstract, BiBTeX, PostScript
Terminological Logics and Conceptual Graphs: An Historical Perspective. Extended Abstract. In Kunze, J. and Stoyan, H. (eds), KI-94 Workshops: Extended Abstracts, Gesellschaft für Informatik, Bonn.
Abstract, BiBTeX, DVI, PostScript
Representations as Full Peirce algebras: Extended Abstract. Manuscript.
Abstract, BiBTeX
Existential Graphs for Terminological Logics. Manuscript.
Abstract, BiBTeX
Peirce Algebras and Relation Algebras are equipollent. Manuscript.
Abstract, BiBTeX
1993
Terminological Representation, Natural Language and Relation Algebra. In Ohlbach, H. J. (Ed.), Proc. of the sixteenth German AI Conf. (GWAI'92), Lecture Notes in Artificial Intelligence Vol. 671, Springer, Berlin, 357-371.
Abstract, BiBTeX, PostScript
Editorial: The possibility of generating true conjectures. Together with H. J. Ohlbach. Journal of Logic and Computation, 3(4), 341-343.
BiBTeX.
1992
Subsumption Computed Algebraically. Together with C. Brink. Computers and Mathematics with Applications 23 (2-9), Special edition on Semantic Networks in Artificial Intelligence, 329-342.
Abstract, BiBTeX, DOI Link.
MOTEL User Manual. Together with U. Hustadt A. Nonnengart and J. Timm. Tech. Rep. MPI-I-92-236, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, DVI, PostScript
1991
Autodescriptivity: Beware! Together with C. Brink and I.M. Rewitzky. The Computer Journal 34 (4), 380-381.
Abstract, BiBTeX, DOI Link.
Algebraic Terminological Representation. Tech. Rep. MPI-I-91-216, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, DVI, PostScript

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 24 May 16
Copyright © 1996-2016 Renate A. Schmidt, School of Computer Science, Univ. Man., schmidt@cs.man.ac.uk