Abstract
This paper describes the major results on research and development of a model generation theorem prover MGTP. It exploits OR parallelism for non-Horn problems and AND parallelism for Horn problems achieving more than a 200-fold speedup on a parallel inference machine PIM with 256 processing elements. With MGTP, we succeeded in proving difficult mathematical problems that cannot be proven on sequential systems, including several open problems in finite algebra.
To enhance the pruning ability of MGTP, several new features are added to it. These include: CMGTP and IV-MGTP to deal with constraint satisfaction problems, enabling negative and interval constraint propagation, respectively, non-Horn magic set to suppress the generation of useless model candidates caused by irrelevant clauses, a proof simplification method to eliminate duplicated subproofs, and MM-MGTP for minimal model generation.
We studied several techniques necessary for the development of applications, such as negation as failure, abductive reasoning and modal logic systems, on MGTP. These techniques share a basic idea, which is to use MGTP as a meta-programming system for each application.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Franz Baader and Bernhard Hollunder. How to prefer more specific defaults in terminological default logic. In Proc. International Joint Conference on Artificial Intelligence, pages 669–674, 1993.
Peter Baumgartner, Ulrich Furbach, and Ilkka Niemelä. Hyper Tableaux. In José Júlio Alferes, Luís Moniz Pereira, and Ewa OrJlowska, editors, Proc. European Workshop: Logics in Artificial Intelligence, JELIA, volume 1126 of Lecture Notes in Artificial Intelligence, pages 1–17. Springer-Verlag, 1996.
Frank Bennett. Quasigroup Identities and Mendelsohn Designs. Canadian Journal of Mathematics, 41:341–368, 1989.
Gerhard Brewka. Preferred subtheories: An extended logical framework for default reasoning. In Proc. International Joint Conference on Artificial Intelligence, pages 1043–1048, Detroit, MI,USA, 1989.
Gerhard Brewka. Adding priorities and specificity to default logic. In Proc. JELIA 94, pages 247–260, 1994.
Gerhard Brewka. Reasoning about priorities in default logic. In Proc. AAAI 94, pages 940–945, 1994.
Gerhard Brewka. Well-founded semantics for extended logic programs with dynamic preference. Journal of Artificial Intelligence Research, 4:19–36, 1996.
Gerhard Brewka and Thomas F. Gordon. How to Buy a Porsche: An Approach to defeasible decision making. In Proc. AAA94 workshop on Computational Dialectics, 1994.
François Bry. Query evaluation in recursive databases: bottom-up and top-down reconciled. Data & Knowledge Engineering, 5:289–312, 1990.
François Bry and Adnan Yahya. Minimal Model Generation with Positive Unit Hyper-Resolution Tableaux. In Proc. 5th International Workshop, TABLEAUX’96, volume 1071 of Lecture Notes in Artificial Intelligence, pages 143–159, Terrasini, Palermo, Italy, May 1996. Springer-Verlag.
Hiroshi Fujita and Ryuzo Hasegawa. A Model-Generation Theorem Prover in KL1 Using Ramified Stack Algorithm. In Proc. 8th International Conference on Logic Programming, pages 535–548. The MIT Press, 1991.
Masayuki Fujita, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Model Generation Theorem Provers on a Parallel Inference Machine. In Proc. International Conference on Fifth Generation Computer Systems, volume 1, pages 357–375, Tokyo, Japan, June 1992.
Masayuki Fujita, John Slaney, and Frank Bennett. Automatic Generation of Some Results in Finite Algebra. In Proc. International Joint Conference on Artificial Intelligence, 1993.
Tetsuro Fujita, Takashi Chikayama, Kazuaki Rokuwasa, and Akihiko Nakase. KLIC: A Portable Implementation of KL1. In Proc. International Conference on Fifth Generation Computer Systems, pages 66–79, Tokyo, Japan, December 1994.
Michael Gelfond and Vladimir Lifschitz. The Stable Model Semantics for Logic Programming. In Proc. 5th International Conference and Symposium on Logic Programming, pages 1070–1080. MIT Press, 1988.
Michael Gelfond and Vladimir Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9:365–385, 1991.
Benjamin Grosof. Generalization Prioritization. In Proc. 2nd Conference on Knowledge Representation and Reasoning, pages 289–300, 1991.
Reiner Hähnle. Tableaux and related methods. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I. North-Holland, 2001.
Reiner Hähnle, Ryuzo Hasegawa, and Yasuyuki Shirai. Model Generation Theorem Proving with Finite Interval Constraints. In Proc. First International Conference on Computational Logic (CL2000), 2000.
Ryuzo Hasegawa and Hiroshi Fujita. Implementing a Model-Generation Based Theorem Prover MGTP in Java. Research Reports on Information Science and Electrical Engineering, 3(1):63–68, 1998.
Ryuzo Hasegawa and Hiroshi Fujita. A new Implementation Technique for a Model-Generation Theorem Prover to Solve Constraint Satisfaction Problems. Research Reports on Information Science and Electrical Engineering, 4(1):57–62, 1999.
Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura. MGTP: A Parallel Theorem-Proving System Based on Model Generation. In Proc. 11th International Conference on Applications of Prolog, pages 34–41, Tokyo, Japan, September 1998.
Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura. Efficient Minimal Model Generation Using Branching Lemmas. In Proc. 17th International Conference on Automated Deduction, volume 1831 of Lecture Notes in Artificial Intelligence, pages 184–199, Pittsburgh, Pennsylvania, USA, June 2000. Springer-Verlag.
Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, and Miyuki Koshimura. Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving. In Proc. 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Artificial Intelligence, pages 176–190, Townsville, North Queensland, Australia, July 1997. Springer-Verlag.
Ryuzo Hasegawa and Miyuki Koshimura. An AND Parallelization Method for MGTP and Its Evaluation. In Proc. First International Symposium on Parallel Symbolic Computation, Lecture Notes Series on Computing, pages 194–203. World Scientific, September 1994.
Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Lazy Model Generation for Improving the Efficiency of Forward Reasoning Theorem Provers. In Proc. International Workshop on Automated Reasoning, pages 221–238, Beijing, China, July 1992.
Ryuzo Hasegawa, Katsumi Nitta, and Yasuyuki Shirai. The Development of an Argumentation Support System Using Theorem Proving Technologies. In Research Report on Advanced Software Enrichment Program 1997, pages 59–66. Information Promotion Agency, Japan, 1999. (in Japanese).
Ryuzo Hasegawa and Yasuyuki Shirai. Constraint Propagation of CP and CMGTP: Experiments on Quasigroup Problems. In Proc. Workshop 1C (Automated Reasoning in Algebra), CADE-12, Nancy, France, 1994.
Katsumi Inoue, Miyuki Koshimura, and Ryuzo Hasegawa. Embedding Negation as Failure into a Model Generation Theorem Prover. In Proc. 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 400–415, Saratoga Springs, NY, USA, 1992. Springer-Verlag.
Katsumi Inoue, Yoshihiko Ohta, Ryuzo Hasegawa, and Makoto Nakashima. Bottom-Up Abduction by Model Generation. In Proc. International Joint Conference on Artificial Intelligence, pages 102–108, 1993.
Miyuki Koshimura and Ryuzo Hasegawa. Modal Propositional Tableaux in a Model Generation Theorem Prover. In Proc. 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 145–151, May 1994.
Miyuki Koshimura and Ryuzo Hasegawa. Proof Simplification for Model Generation and Its Applications. In Proc. 7th International Conference, LPAR 2000, volume 1955 of Lecture Notes in Artificial Intelligence, pages 96–113. Springer-Verlag, November 2000.
Robert A. Kowalski and Francesca Toni. Abstract Argumentation. Artificial Intelligence and Law Journal, 4:275–296, 1996.
Reinhold Letz, Klaus Mayr, and Christoph Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13:297–337, 1994.
Vladimir Lifschitz. Computing Circumscription. In Proc. International Joint Conference on Artificial Intelligence, pages 121–127, Los Angeles, CA, USA, 1985.
Donald W. Loveland, David W. Reed, and Debra S. Wilson. Satchmore: Satchmo with RElevancy. Journal of Automated Reasoning, 14(2):325–351, April 1995.
James J. Lu. Logic Programming with Signs and Annotations. Journal of Logic and Computation, 6(6):755–778, 1996.
Rainer Manthey and Francoois Bry. SATCHMO: a theorem prover implemented in Prolog. In Proc. 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 415–434, Argonne, Illinois, USA, May 1988. Springer-Verlag.
William McCune and Larry Wos. Experiments in Automated Deduction with Condensed Detachment. In Proc. 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 209–223, Saratoga Springs, NY, USA, 1992. Springer-Verlag.
Jack Minker. On indefinite databases and the closed world assumption. In Proc. 6th International Conference on Automated Deduction, volume 138 of Lecture Notes in Computer Science, pages 292–308, Courant Institute, USA, 1982. Springer-Verlag.
Ugo Montanari and Francesca Rossi. Finite Domain Constraint Solving and Constraint Logic Programming. In Constraint Logic Programming: Selected Research, pages 201–221. The MIT press, 1993.
Hiroshi Nakashima, Katsuto Nakajima, Seiichi Kondo, Yasutaka Takeda, Yū Ina-mura, Satoshi Onishi, and Kanae Matsuda. Architecture and Implementation of PIM/m. In Proc. International Conference on Fifth Generation Computer Systems, volume 1, pages 425–435, Tokyo, Japan, June 1992.
Ilkka Niemelä. A Tableau Calculus for Minimal Model Reasoning. In Proc. 5th International Workshop, TABLEAUX’96, volume 1071 of Lecture Notes in Artificial Intelligence, pages 278–294, Terrasini, Palermo, Italy, May 1996. Springer-Verlag.
Katsumi Nitta, Yoshihisa Ohtake, Shigeru Maeda, Masayuki Ono, Hiroshi Ohsaki, and Kiyokazu Sakane. HELIC-II: A Legal Reasoning System on the Parallel Inference Machine. In Proc. International Conference on Fifth Generation Computer Systems, volume 2, pages 1115–1124, Tokyo, Japan, June 1992.
Yoshihiko Ohta, Katsumi Inoue, and Ryuzo Hasegawa. On the Relationship Between Non-Horn Magic Sets and Relevancy Testing. In Proc. 15th International Conference on Automated Deduction, volume 1421 of Lecture Notes in Artificial Intelligence, pages 333–349, Lindau, Germany, July 1998. Springer-Verlag.
Franz Oppacher and E. Suen. HARP: A Tableau-Based Theorem Prover. Journal of Automated Reasoning, 4:69–100, 1988.
Henry Prakken and Giovanni Sartor. Argument-based Extended Logic Programming with Defeasible Priorities. Journal of Applied Non-Classical Logics, 7:25–75, 1997.
Chiaki Sakama and Katsumi Inoue. Representing Priorities in Logic Programs. In Proc. International Conference and Symposium on Logic Programming, pages 82–96, 1996.
Heribert Schütz and Tim Geisler. Efficient Model Generation through Compilation. In Proc. 13th International Conference on Automated Deduction, volume 1104 of Lecture Notes in Artificial Intelligence, pages 433–447. Springer-Verlag, 1996.
Yasuyuki Shirai and Ryuzo Hasegawa. Two Approaches for Finite-domain Constraint Satisfaction Problem-CP and MGTP-. In Proc. 12th International Conference on Logic Programming, pages 249–263. MIT Press, 1995.
Mark Stickel. The Path-Indexing Method For Indexing Terms. Technical Note 473, AI Center, SRI, 1989.
Mark E. Stickel. Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction. Journal of Automated Reasoning, 13(2):189–210, October 1994.
Geoff Sutcliffe, Christian Suttner, and Theodor Yemenis. The TPTP Problem Library. In Proc. 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 252–266, Nancy, France, 1994. Springer-Verlag.
Evan Tick and Miyuki Koshimura. Static Mode Analyses of Concurrent Logic Programs. Journal of Programming Languages, 2:283–312, 1994.
Kazunori Ueda and Takashi Chikayama. Design of the Kernel Language for the Parallel Inference Machine. Computer Journal, 33:494–500, December 1990.
Debra S. Wilson and Donald W. Loveland. Incorporating Relevancy Testing in SATCHMO. Technical Reports CS-1989-24, Department of Computer Science, Duke University, Durham, North Carolina, USA, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hasegawa, R., Fujita, H., Koshimura, M., Shirai, Y. (2002). A Model Generation Based Theorem Prover MGTP for First-Order Logic. In: Kakas, A.C., Sadri, F. (eds) Computational Logic: Logic Programming and Beyond. Lecture Notes in Computer Science(), vol 2408. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45632-5_8
Download citation
DOI: https://doi.org/10.1007/3-540-45632-5_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43960-8
Online ISBN: 978-3-540-45632-2
eBook Packages: Springer Book Archive