Kyushu University Academic Staff Educational and Research Activities Database
Researcher information (To researchers) Need Help? How to update
Miyuki Koshimura Last modified date:2017.05.02



Graduate School
Undergraduate School


Homepage
http://opal.inf.kyushu-u.ac.jp/~koshimura
Academic Degree
Doctor of Engineer
Field of Specialization
Automated Reasoning Systems and Their Applications
Research
Research Interests
  • Automated Reasoning and its Applications
    keyword : model generation, non-monotonic logic, efficiency of inference, verification
    1995.04Automated Resoning: (1)Developing a mechnicial theorem proving system based on model generation (2)Enhancing efficiency of model generation by using proof condensation and folding-up operations (3)Implementing modal reasoning on top of model generation (4)Verifying a railway interlocking system with a mathematical method (5)SAT solver and its applications.
  • Parallel Operating System
    keyword : parallel inference machine, parallel OS
    1986.11~1990.03.
Academic Activities
Papers
1. 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, E97-D, 7, 2014.07.
2. Xiaojuan Liao, Miyuki Koshimura, RYUZO HASEGAWA, Solving the Coalition Structure Generation Problem with MaxSAT, 24th International Conference on Tools with Artificial Intelligence, 2012.12.
3. 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.
4. 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.
5. Miyuki Koshimura, Hidetomo Nabeshima, HIROSHI FUJITA, RYUZO HASEGAWA, Solving Open Job-Shop Scheduling Problems by SAT Encoding, IEICE TRANSACTIONS on Information and Systems, E93-D, 8 , 2316-2318, 2010.08.
6. Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, and Ryuzo Hasegawa, Minimal Model Generation with respect to an Atom Set, International Workshops on First-Order Theorem Proving (FTP), 49-59, 2009.07.
7. Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03.
8. Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12.
9. Miyuki Koshimura, Ryuzo Hasegawa, Proof Simplification for Model Generation and Its Applications, Proc. of LPAR2000, 1955, 96-113, LNAI1955, 2000.11.
10. 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.
11. 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.
12. Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09.
13. Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05.
14. Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06.
15. 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.
Works, Software and Database
1. QMaxSAT: Q-dai MaxSAT solver
[URL].
Other Research Activities
  • 2013.07, QMaxSAT was placed second in the industrial subcategory of partial Max-SAT category of the 2013 MaxSAT evaluation..
  • 2012.06, QMaxSAT was placed first in both the industrial subcategory and the crafted subcategory of partial Max-SAT category of the 2012 MaxSAT evaluation..
  • 2011.06, QMaxSAT(Q-dai MaxSAT Solver) was placed first in the industrial subcategory and second in the crafted subcategory of partial Max-SAT category of the 2011 MaxSAT evaluation..
  • 2010.07, QMaxSAT(Q-dai MaxSAT Solver) was placed first in the industrial subcategory and second in the crafted subcategory of partial Max-SAT category of the 2010 MaxSAT evaluation..
Membership in Academic Society
  • The Institute of Electronics, Information and Communication Engineers
  • Japan Society for Artificial Intelligence
  • Information Processing Society of Japan
  • Japan Society for Software and Technology