$B!J#5#4!KK!E*?dO@

	$B%^(B $B%7(B $B%s!'(BPIM, Multi-PSI
	$B4D!!!!6-!'(BPIMOS
	$B8@!!!!8l!'(BKL1
	$B%=!<%9NL!'(B1.7 MB
	$BJ8!!!!=q!'%^%K%e%"%k(B ($B1Q8l(B)

---

$B35MW(B

$BK!N'>rJ8$HH=Nc$r;H$C$?K!E*?dO@$rJBNs?dO@$K$h$C$F9T$&%7%9%F%`!#(B

$B9=@.(B

$B5!G=(B

HELLIC-II$B$OM?$($i$l$?;v7o$K4X$9$kK!E*7kO@$r!"K!NaJ8$H2a5n$NH=Nc$r;2>H(B $B$9$k$3$H$K$h$C$FF3$-$@$7!"?dO@LZ$N7A$G$=$l$i$r=PNO$9$k%7%9%F%`$G$"$k!#(B

$BK!N'$NCN<1$OK!NaJ8$H2a5n$NH=Nc$+$i$J$k!#(B

$BK!NaJ8$OK!N'%k!<%k$N=89g$G$"$k$+$i!"K!NaJ8$K4p$E$/?dO@$O%k!<%k%Y!<%9?d(B $BO@$H$7$F $BK!N'%k!<%k$O$7$P$7$PDj5A$N[#Kf$JK!N'MQ8l(B ($BK!E*35G0(B) $B$r4^$s$G$$$k$?$a!"(B $BK!E*35G0$H6qBNE*$J;vH$7!"$=$NCf$NO@M}E8(B $B3+$r:FMxMQ$9$k;vNc%Y!<%9?dO@$r$*$3$J$&I,MW$,$"$j!"$3$l$i(B2$B $B%k!<%k%Y!<%9%(%s%8%s$OK!N'%k!<%k$r;2>H$7$F!"K!E*7kO@$r1iehE*$KF3$/!#$3(B $B$N%(%s%8%s$OJBNsDjM}>ZL@4o(B MGTP (Model Generation Theorem Prover) $B$r%Y!<(B $B%9$K!"$$$/$D$+$N5!G=$rDI2C$7$?$b$N$G$"$k!#(B

$B;vNc%Y!<%9%(%s%8%s$ON`;w$N;vNc$r8!:w$7!"$=$N;vNc$N%k!<%k$r?7$?$J;vNc$K(B $BE,MQ$9$k$3$H$K$h$C$F!"?7$?$JO@M}$r9=C[$9$k$H$$$&7A;;NL$NB?$$=hM}$rJBNs(B $B=hM}$K$h$j9bB.2=$7$F$$$k!#(B

$B#F#T#P(B

• $BK!E*?dO@

---

www-admin@icot.or.jp