MGTP swMATH ID: 9701 Software Authors: Hasegawa, Ryuzo; Fujita, Hiroshi; Koshimura, Miyuki; Shirai, Yasuyuki Description: A model generation based theorem prover MGTP for first-order logic. 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. Homepage: http://link.springer.com/chapter/10.1007/BFb0027401 Related Software: SATCHMO; TPTP; MiniSat; FINDER; QMaxSAT; Scsat; RRL; FALCON; ModGen; Mace4; E-Darvin; SCOTT; SATO; Darwin; OTTER; 3TAP; InKa; SETHEO Cited in: 6 Publications all top 5 Cited by 15 Authors 3 Hasegawa, Ryuzo 3 Koshimura, Miyuki 2 Fujita, Hiroshi 2 Zhang, Jian 1 Ahrendt, Wolfgang 1 Beckert, Bernhard 1 Hähnle, Reiner 1 Inoue, Katsumi 1 Menzel, Wolfram 1 Ohta, Yoshihiko 1 Reif, Wolfgang 1 Schellhorn, Gerhard 1 Schmitt, Peter H. 1 Shirai, Yasuyuki 1 Zhang, Hantao Cited in 1 Serial 1 Journal of Computer Science and Technology Cited in 2 Fields 6 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year