Abstract
This paper offers an informal overview and discussion on first order predicate logic reasoning systems together with a description of applications which are carried out in the Artificial Intelligence Research Group of the University in Koblenz. Furthermore the technique of knowledge compilation is shortly introduced.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahrendt, W., et al.: The KeY System: Integrating Object-Oriented Design and Formal Methods. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, pp. 327–330. Springer, Heidelberg (2002)
Baader, F., et al. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
Baumgartner, P., Furbach, U.: Calculi for Disjunctive Logic Programming. In: Maluszynski, J. (ed.) Logic Programming - Proceedings of the 1997 International Symposium, New York, The MIT Press, Cambridge (1997)
Baumgartner, P., et al.: Model Based Deduction for Database Schema Reasoning. In: Biundo, S., Frühwirth, T., Palm, G. (eds.) KI 2004. LNCS (LNAI), vol. 3238, pp. 168–182. Springer, Heidelberg (2004)
Baumgartner, P., et al.: Living Book - Deduction, Slicing, and Interaction. J. Autom. Reasoning 32(3), 259–286 (2004)
Baumgartner, P., Furbach, U., Niemelä, I.: Hyper Tableaux. In: Orłowska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1–17. Springer, Heidelberg (1996)
Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 19–99. Elsevier, Amsterdam (2001)
Beckert, B., et al.: The Tableau-based Theorem Prover \(_{\mbox{3}}\)T\(^{\mbox{A}}\)P Version 4.0. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 303–307. Springer, Heidelberg (1996)
Darwiche, A.: Decomposable Negation Normal Form. Journal of the ACM 48(4) (2001), citeseer.ist.psu.edu/477720.html
Darwiche, A.: New Advances in Compiling CNF into Decomposable Negation Normal Form. In: Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI’2004, pp. 328–332 (2004)
Dix, J., Furbach, U., Niemelä, I.: Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1241–1354. Elsevier, Amsterdam (2001)
Furbach, U., et al.: Issues Management: Erkennen und Beherrschen von kommunikativen Risiken und Chancen. Fachberichte Informatik 2–2004, Universität Koblenz-Landau, Institut für Informatik, Koblenz (2004)
Furbach, U.: AI – A Multiple Book Review. Artificial Intelligence 145(1-2), 245 (2003)
Henzinger, T.A.: The Theory of Hybrid Automata. In: Proceedings of the IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Hillenbrand, T., Löchner, B.: The Next WALDMEISTER Loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 486–500. Springer, Heidelberg (2002)
Kowalski, R.A., Kuehner, D.: Linear Resolution with Selection Function. Artificial Intelligence 2, 227–260 (1971)
Kleemann, T., Sinner, A.: Decision Support for Personalization on Mobile Devices. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 404–406. Springer, Heidelberg (2005)
Kleemann, T., Sinner, A.: Krhyper - in your Pocket, System Description. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 452–458. Springer, Heidelberg (2005)
Loveland, D.: Mechanical Theorem Proving by Model Elimination. JACM 15(2) (1968)
Massacci, F.: Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 14–18. Springer, Heidelberg (1999)
McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 663–664. Springer, Heidelberg (1990)
McCune, W.: Solution of the Robbins Problem. J. Autom. Reasoning 19(3), 263–276 (1997)
Poole, D., Mackworth, A., Goebel, R.: Computational Intelligence: A Logical Approach. Oxford University Press, Oxford (1997)
Pelletier, F., Sutcliffe, G., Suttner, C.: The Development of CASC. AI Communications 15(2-3), 79–90 (2002)
Robinson, J.A., Voronkov, A.: Handbook of Automated Reasoning (in 2 volumes). Elsevier, Amsterdam (2001)
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002)
Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004)
Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)
Weidenbach, C.: Spass - version 0.49. Journal of Automated Reasoning 18(2), 247–252 (1997)
Wernhard, C.: System Description: KRHyper. Fachberichte Informatik 14–2003, Universität Koblenz-Landau, Institut für Informatik, Koblenz (2003)
Wernhard, C.: Tableaux Between Proving, Projection and Compilation. Technical report, Universität Koblenz-Landau. In preparation (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Furbach, U., Obermaier, C. (2007). Applications of Automated Reasoning. In: Freksa, C., Kohlhase, M., Schill, K. (eds) KI 2006: Advances in Artificial Intelligence. KI 2006. Lecture Notes in Computer Science(), vol 4314. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69912-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-69912-5_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69911-8
Online ISBN: 978-3-540-69912-5
eBook Packages: Computer ScienceComputer Science (R0)