Kyushu University Academic Staff Educational and Research Activities Database
List of Papers
Miyuki Koshimura Last modified date:2021.10.20

Assistant Professor / Intelligence Science / Department of Informatics / Faculty of Information Science and Electrical Engineering


Papers
1. Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu, Fagen Li, Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial MaxSAT, Mathematical Problems in Engineering, https://doi.org/10.1155/2021/9615463, 2021, 17, 2021.07.
2. Aolong Zha, Rongxuan Gao, Qiong Chang, Miyuki Koshimura, Itsuki Noda, CNF Encodings for the Min-Max Multiple Traveling Salesmen Problem, 32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020, 10.1109/ICTAI50040.2020.00053, 285-292, 2021.01.
3. Miyuki Koshimura, Ken Satoh, A Simple yet Efficient MCSes Enumeration with SAT Oracles, 12th Asian Conference on Intelligent Information and Database Systems, 10.1007/978-3-030-41964-6_17, Part I, 191-201, 2020.03.
4. Emi Watanabe, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo, Solving Coalition Structure Generation Problems over Weighted Graph, PRIMA 2019: Principles and Practice of Multi-Agent Systems - 22nd International Conference, 10.1007/978-3-030-33792-6_21, 338-353, 2019.10.
5. Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu, Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems, PRICAI 2019: 16th Pacific Rim International Conference on Artificial Intelligence, 10.1007/978-3-030-29908-8_49, 1, 618-631, 2019.08.
6. Xiaojuan Liao, Miyuki Koshimura, A comparative analysis and improvement of MaxSAT encodings for coalition structure generation under MC-nets, Journal of Logic and Computation, 10.1093/logcom/exz017, 29, 913-931, 2019.10, Coalition structure generation (CSG) is one of the main research issues in the use of coalitional games in multiagent systems and weighted partial MaxSAT (WPM) encodings, i.e. rule relation-based WPM (RWPM) and agent relation-based WPM (AWPM), which are efficient for solving the CSG problem. Existing studies show that AWPM surpasses RWPM since it achieves more compact encoding; it generates fewer variables and clauses than RWPM. However, in this paper, we focus on a special case in which the two encodings generate identical numbers of variables and clauses. Experiments show that RWPM surprisingly has a dominant advantage over AWPM, which aroused our interest. We exploit the deep-rooted reason and find that it is the redundancy when encoding transitive laws in RWPM that leads to this situation. Finally, we remove redundant clauses for transitive laws in RWPM and develop an improved RWPM with refined transitive laws to solve the CSG problem. Experiments demonstrate that refined encoding is more compact and efficient than previous WPM encodings..
7. Aolong Zha, Miyuki Koshimura, Hiroshi Fujita, N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT, Constraints, 10.1007/s10601-018-9299-0, 24, 2, 133-161, 2019.04, Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver..
8. Xiaojuan Liao, Miyuki Koshimura, Kazuki Nomoto, Suguru Ueda, Yuko Sakurai, Makoto Yokoo, Improved WPM encoding for coalition structure generation under MC-nets, Constraints, 10.1007/s10601-018-9295-4, 24, 1, 25-55, 2019.01, The Coalition Structure Generation (CSG) problem plays an important role in the domain of coalition games. Its goal is to create coalitions of agents so that the global welfare is maximized. To date, Weighted Partial MaxSAT (WPM) encoding has shown high efficiency in solving the CSG problem, which encodes a set of constraints into Boolean propositional logic and employs an off-the-shelf WPM solver to find out the optimal solution. However, in existing WPM encodings, a number of redundant encodings are asserted. This results in additional calculations and correspondingly incurs performance penalty. Against this background, this paper presents an Improved Rule Relation-based WPM (I-RWPM) encoding for the CSG problem, which is expressed by a set of weighted rules in a concise representation scheme called Marginal Contribution net (MC-net). In order to effectively reduce the constraints imposed on encodings, we first identify a subset of rules in an MC-net, referred as a set of freelance rules. We prove that solving the problem made up of all freelance rules can be achieved with a straightforward means without any extra encodings. Thus the set of rules requiring to be encoded is downsized. Next, we improve the encoding of transitive relations among rules. To be specific, compared with the existing rule relation-based encoding that generates transitive relations universally among all rules, I-RWPM only considers the transitivity among rules with particular relationship. In this way, the number of constraints to be encoded can be further decreased. Experiments suggest that I-RWPM significantly outperforms other WPM encodings for solving the same set of problem instances.
提携構造形成問題(CSG)は協力ゲーム理論の問題の一つで、エージェント集合を社会的効用が最大となるように分割する問題である. 我々は以前、CSGをMaxSAT符号化して解く解法を示した. この解法は従来の混合整数計画法を利用する手法より桁違いに速い. 本論文では、このMaxSAT符号化による制約数を削減する手法を提案した. そして理論的には、制約数を少なくとも1/4以下に削減できることを示した. 計算機実験では、エージェント数が300の時、制約数は10の7乗超から10の5乗程度に削減、計算時間は100秒超から10秒以内に短縮できた..
9. Aolong Zha, Miyuki Koshimura, Hiroshi Fujita, A Hybrid Encoding of Pseudo-Boolean Constraints into CNF, Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017, 10.1109/TAAI.2017.15, 9-12, 2017.12.
10. Aolong Zha, Naoki Uemura, Miyuki Koshimura, HIROSHI FUJITA, Mixed Radix Weight Totalizer Encoding for Pseudo-Boolean Constraints, 29th International Conference on Tools with Artificial Intelligence, 10.1109/ICTAI.2017.00135, 868-875, 2017.11.
11. Aolong Zha, Kazuki Nomoto, Suguru Ueda, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo, Coalition Structure Generation for Partition Function Games Utilizing a Concise Graphical Representation, 20th International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2017 PRIMA 2017 Principles and Practice of Multi-Agent Systems - 20th International Conference, Proceedings, 10.1007/978-3-319-69131-2_9, 143-159, 2017.01, Coalition Structure Generation (CSG), a main research issue in the domain of coalition games, involves partitioning agents into exhaustive and disjoint coalitions to optimize the social welfare. The advent of compact representation schemes, such as Partition Decision Trees (PDTs), promotes the efficiency of solving CSG problems. This paper studies the CSG problem for partition function games (PFGs) which are coalitional games with externalities. In PFGs, each value of a coalition depends on how the other agents are partitioned. We apply PDTs to represent PFGs and present two methods to solve CSG problems: a depth-first branch-and-bound algorithm and MaxSAT encoding..
12. Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Reconstructing AES Key Schedule Images with SAT and MaxSAT, IEICE TRANSACTIONS on Information and Systems, 10.1587/transinf.2015EDP7223, E99D, 1, 141-150, 2016.01, Cold boot attack is a side channel attack that recovers data from memory, which persists for a short period after power is lost. In the course of this attack, the memory gradually degrades over time and only a corrupted version of the data may be available to the attacker. Recently, great efforts have been made to reconstruct the original data from a corrupted version of AES key schedules, based on the assumption that all bits in the charged states tend to decay to the ground states while no bit in the ground state ever inverts. However, in practice, there is a small number of bits flipping in the opposite direction, called reverse flipping errors. In this paper, motivated by the latest work that formulates the relations of AES key bits as a Boolean Satisfiability problem, we move one step further by taking the reverse flipping errors into consideration and employing off-the-shelf SAT and MaxSAT solvers to accomplish the recovery of AES-128 key schedules from decayed memory images. Experimental results show that, in the presence of reverse flipping errors, the MaxSAT approach enables reliable recovery of key schedules with significantly less time, compared with the SAT approach that relies on brute force search to find out the target errors. Moreover, in order to further enhance the efficiency of key recovery, we simplify the original problem by removing variables and formulas that have relatively weak relations to the whole key schedule. Experimental results demonstrate that the improved MaxSAT approach reduces the scale of the problem and recover AES key schedules more efficiently when the decay factor is relatively large..
13. Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, MaxSAT Encoding for MC-Net-Based Coalition Structure Generation Problem with Externalities, IEICE TRANSACTIONS on Information and Systems, 10.1587/transinf.E97.D.1781, E97-D, 7, 1781-1789, 2014.07, Coalition Structure Generation (CSG) means partitioning agents into exhaustive and disjoint coalitions so that the sum of values of all the coalitions is maximized. Solving this problem could be facilitated by employing some compact representation schemes, such as marginal contribution network (MC-net). In MC-net, the CSG problem is represented by a set of rules where each rule is associated with a real-valued weights, and the goal is to maximize the sum of weights of rules under some constraints. This naturally leads to a combinatorial optimization problem that could be solved with weighted partial MaxSAT (WPM). In general, WPM deals with only positive weights while the weights involved in a CSG problem could be either positive or negative. With this in mind, in this paper, we propose an extension of WPM to handle negative weights and take advantage of the extended WPM to solve the MC-net-based CSG problem. Specifically, we encode the relations between each pair of agents and reform the MC-net as a set of Boolean formulas. Thus, the CSG problem is encoded as an optimization problem for WPM solvers. Furthermore, we apply this agent relation-based WPM with minor revision to solve the extended CSG problem where the value of a coalition is affected by the formation of other coalitions, a coalition known as externality. Experiments demonstrate that, compared to the previous encoding, our proposed method speeds up the process of solving the CSG problem significantly, as it generates fewer number of Boolean variables and clauses that need to be examined by WPM solver..
14. Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Extending MaxSAT to Solve the Coalition Structure Generation Problem with Externalities Based on Agent Relations, IEICE TRANSACTIONS on Information and Systems, 10.1587/transinf.E97.D.1812, E97-D, 7, 1812-1821, 2014.07, Coalition Structure Generation (CSG) means partitioning agents into exhaustive and disjoint coalitions so that the sum of values of all the coalitions is maximized. Solving this problem could be facilitated by employing some compact representation schemes, such as marginal contribution network (MC-net). In MC-net, the CSG problem is represented by a set of rules where each rule is associated with a real-valued weights, and the goal is to maximize the sum of weights of rules under some constraints. This naturally leads to a combinatorial optimization problem that could be solved with weighted partial MaxSAT (WPM). In general, WPM deals with only positive weights while the weights involved in a CSG problem could be either positive or negative. With this in mind, in this paper, we propose an extension of WPM to handle negative weights and take advantage of the extended WPM to solve the MC-net-based CSG problem. Specifically, we encode the relations between each pair of agents and reform the MC-net as a set of Boolean formulas. Thus, the CSG problem is encoded as an optimization problem for WPM solvers. Furthermore, we apply this agent relation-based WPM with minor revision to solve the extended CSG problem where the value of a coalition is affected by the formation of other coalitions, a coalition known as externality. Experiments demonstrate that, compared to the previous encoding, our proposed method speeds up the process of solving the CSG problem significantly, as it generates fewer number of Boolean variables and clauses that need to be examined by WPM solver..
15. Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers, 25th International Conference on Tools with Artificial Intelligence, 10.1109/ICTAI.2013.13, 9-17, 2013.11.
16. Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Using MaxSAT to Correct Errors in AES Key Schedule Images, 25th International Conference on Tools with Artificial Intelligence, 10.1109/ICTAI.2013.51, 284-291, 2013.11.
17. HIROSHI FUJITA, Miyuki Koshimura, RYUZO HASEGAWA, SCSat: A Soft Constraint Guided SAT Solver, 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), 415-421, 2013.07.
18. Xiaojuan Liao, Miyuki Koshimura, RYUZO HASEGAWA, Solving the Coalition Structure Generation Problem with MaxSAT, 24th International Conference on Tools with Artificial Intelligence, 910-915, 2012.12.
19. Xue-Feng Zhang, Miyuki Koshimura, HIROSHI FUJITA, RYUZO HASEGAWA, Hybrid Particle Swarm Optimization and Convergence Analysis for Scheduling Problems, Evolutionary Computation and Multi-Agent Systems and Simulation (ECoMASS) Workshop, 307-314, 2012.07.
20. Noriacki Chikara, Miyuki Koshimura, HIROSHI FUJITA, RYUZO HASEGAWA, Rule Extraction from Micro-Blog using Inductive Logic Programming, 2012 Spring World Congress on Engineering and Technology (SCET2012), 2, 257-260, 2012.05.
21. Yuichi Takiguchi, Koji Kurakado, Tetsuya Oishi, Miyuki Koshimura, Hiroshi Fujita, and Ryuzo Hasegawa, Evaluating Reranking Methods based on Link Co-occurence and Category in Wikipedia, 4th International Conference on Agents and Artificial Intelligence, 1, 277-282, 2012.02.
22. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa, QMaxSAT: A Partial Max-SAT Solver, Journal on Satisfiability, Boolean Modeling and Computation, 8, 95-100, 2012.01, We present a partial Max-SAT solver \QMaxSAT which
uses CNF encoding of Boolean cardinality constraints.
The old version 0.1 was obtained by
adapting a CDCL based SAT solver MiniSat to manage cardinality constraints.
It was placed first in the industrial subcategory and second in the crafted
subcategory of partial Max-SAT category of the 2010 Max-SAT Evaluation.

The new version 0.2 is obtained by modifying version 0.1 to
decrease the number of clauses for the cardinality encoding.
We compare the two versions by solving Max-SAT instances taken
from the 2010 Max-SAT Evaluation..
23. Xue-Feng Zhang, Xuanye An, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Hybrid Particle Swarm Optimization with Parameter Selection Approaches to Solve Flow Shop Scheduling Problem, 10th IEEE Internationa Conference on Cybernetic Intelligent Systems, 13-19, 2011.09.
24. Xuanye An, Miyuki Koshimura, Hiroshi Fujita and Ryuzo Hasegawa, QMaxSAT version 0.3 & 0.4, International Workshop on First-Order Theorem Proving (FTP), FTP 2011, TABLEAUX 2011 Workshops, Tutorials, and Short Papers, pp.7-15, 2011.07.
25. Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Combining PSO and Local Search to Solve Scheduling Problems, 10th Annual Conference Companion on Genetic and Evolutionary Computation (GECCO'11), 347-357, 2011.07.
26. Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita and Ryuzo Hasegawa, An Efficient Hybrid Particle Swarm Optimization for the Job Shop Scheduling Problem, IEEE, Proc. of 2011 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE 2011), pp.622-626, 2011.06.
27. Wataru Shirakihara, Tetsuya Oishi, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, TRENDSPOTTER DETECTION SYSTEM FOR TWITTER, Proc. of ICAART 2011, 1, 625-628, International Conference on Agents and Artificial Intelligence, 2011.01.
28. Koji Kurakado, Tetsuya Oishi, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, EVALUATING RERANKING METHODS USING WIKIPEDIA FEATURES, Proc. of ICAART 2011, 1, 376-381, International Conference on Agents and Artificial Intelligence, 2011.01.
29. Xue-Feng Zhang, Bin Tong, Miyuki Koshimura, Hiroshi Fujita, and Ryuzo Hasegawa, A Multi-Layer Hybrid Particle Swarm Optimization Model for Flow Shop Scheduling Problem, Australian Journal of Intelligent Information Processing Systems, 12, 4, 1-6, 7th International Conference on Neural Information Processing (ICONIP 2010), 2010.12.
30. Xue-Feng Zhang, Bin Tong, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, A Hybrid Particle Swarm Optimization Algorithm HPTS for the Flow-Shop Scheduling Problem, 九州大学大学院システム情報科学紀要, 15, 2, 65-69, 2010.09.
31. Noriaki Chikara, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Rule Extraction from Blog Using Inductive Logic Programming, Proc. of WEBPRESS 2010, 269-272, 2010.08.
32. Kentaro Hori, Tetsuya Oishi, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Related Word Extraction from Wikipedia for Web Retrieval Assistance, Proc. of ICAART 2010, 2, 192-199, 2010.01.
33. Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa, Solving open job-shop scheduling problems by SAT encoding, IEICE Transactions on Information and Systems, 10.1587/transinf.E93.D.2316, E93-D, 8, 2316-2318, 2010.01, This paper tries to solve open Job-Shop Scheduling Problems (JSSP) by translating them into Boolean Satisfiability Testing Problems (SAT). The encoding method is essentially the same as the one proposed by Crawford and Baker. The open problems are ABZ8, ABZ9, YN1, YN2, YN3, and YN4. We proved that the best known upper bounds 678 of ABZ9 and 884 of YN1 are indeed optimal. We also improved the upper bound of YN2 and lower bounds of ABZ8, YN2, YN3 and YN4..
34. Tetsuya Oishi, Ttsnenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Related Word Extraction Algorithm for Query Expansion - an Evaluation -, Proc. of ACCDS 2009, 41-56, 2009.12.
35. Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa, Minimal model generation with respect to an atom set, 7th International Workshop on First-Order Theorem Proving, FTP 2009 CEUR Workshop Proceedings, 556, 49-59, 2009.12, This paper studies minimal model generation for SAT instances. In this study, we minimize models with respect to an atom set, and not to the whole atom set. In order to enumerate minimal models, we use an arbitrary SAT solver as a subroutine which returns models of satisfiable SAT instances. In this way, we benefit from the year-byyear progress of efficient SAT solvers for generating minimal models. As an application, we try to solve job-shop scheduling problems by encoding them into SAT instances whose minimal models represent optimum solutions..
36. Tetsuya Oishi, Yoshiaki Kambara, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura, Personalized Search using ODP-based User Profiles Created from User Bookmark, Pacific Rim Int'l Conf. on Artificial Intelligence (PRICAI 2008), 839-848, 2008.12.
37. Tetsuya Oishi, Shunsuke Kuramoto, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, A Method for Query Expansion Using the Related Word Extraction Algorithm, Proc. of WIRSS, 41-44, 2008.12.
38. Tetsuya Oishi, Shunsuke Kuramoto, Hiroto Nagata, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura, User-Schedule-based Web Page Recommendation, The 2007 IEEE/WIC/ACM International Conference on Web Intelligence, pp.776-779, 2007.11.
39. Satoshi Amamiya, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Ryo Hirana, and Makoto Amamiya, A Language Design for Non-Interruptable Multithreading Environment Fuce, International Supercomputing Conference (ISC'07), CD, 2007.06.
40. Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03.
41. Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12.
42. Miyuki Koshimura, Ryuzo Hasegawa, Proof Simplification for Model Generation and Its Applications, Proc. of LPAR2000, 10.1007/3-540-44404-1_8, 1955, 96-113, LNAI1955, 2000.11.
43. Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Efficient Minimal Model Generation Using Branching Lemmas, Proc. of CADE-17, 1831, 184-199, LNAI1831, 2000.06.
44. Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, MGTP: A Parallel Theorem-Proving System Based on Model Generation, Proc. of INAP98, 34-41, 1998.09.
45. Miyuki Koshimura, Takashi Matsumoto, Hiroshi Fujita and Ryuzo Hasegawa, A Method to Eliminate Redundant Case-Splittings in MGTP, IJCAI-97 Workshop on Model Based Automated Reasonging, pp. 73-84, 1997.08.
46. Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura, Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving, Proc. of CADE-14, 1249, 176-190, pp.176-190, 1997.07.
47. Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, MGTP: A Model Generation Theorem Prover - Its Advanced Features and Applications -, Proc. of TABLEAUX'97, 1227, 1-15, 1997.05.
48. Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09.
49. Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05.
50. Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, Lazy Model Generation for Improving the Efficiency of Forward Reasoning Theorem Provers, Proc. of the Intl. Workshop on Automated Reasoning, 192-202, 1992.07.
51. Masayuki Fujita, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, Model Generation Theorem Provers on a Parallel Inference Machine, Proc. of FGCS'92, 357-375, 1992.06.
52. Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06.
53. Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa, Embedding Negation as Failure into a Model Generation Theorem Prover, Proc. of CADE-11, 400-415, 1992.06.