ProofSummit2015sakai_revised
|
|
|
- すずり ありはら
- 6 years ago
- Views:
Transcription
1 SAT/SMT Proof Summit 2015
2 : github: G+: : Haskeller Alloy TaPL SAT/SMT
3 CM: Alloy &TaPL
4 Courserian Coursera Computing for Data Analysis by Roger D. Johns Hopkins University Data Analysis by Jeff Johns Hopkins University Machine Learning by Andrew Stanford University Introduction to Recommender Systems by Joseph A Konstan and Michael D University of Minnesota Process Mining: Data science in Action by Wil van der Eindhoven University of Technology NHK MOOC
5 (1) : SAT SAT = SATisfiability Problem (= )? : (P Q) (P Q) ( P Q) (P = true, Q = false ) : (P Q) (P Q) ( P Q) ( P Q) SAT
6 (2) : SMT SMT = Satisfiability Modulo Theories : 0 b b < 10 (2 b + 1 = c read(a,b) = 0) f(read(write(a,b,3), c-2)) f(c-b+1) a, b, c, f? SAT SMT SAT
7 : SAT NP SAT SAT/SMT (ICFP Programming Contest ) Elegant general-purpose formulations in terms of constraint solving: Relatively easy to code up and obtain decent results But, hand-tuned solutions are going to do better... MUCH BETTER
8 : (Craig s interpolation theorem) - (Löwenheim Skolem theorem) Proof Summit
9 vs. (valid) : M φ for all M : P P, 3 > 2 (satisfiable) : M φ for some M : P Q, 3 > x, P P (unsatisfiable) satisfiable valid unsatisfiable : M φ for all M : P P, x > 2 0 x ( ) ( )
10 SAT
11 SAT B.C. (Before Chaff) 1960 DP 10 var 1988 SOCRATES 3k var 1994 Hannibal 3k var GRASP SATO 1k var 1k var 1962 DLL 10 var 1986 BDD 100 var 1992 GSAT 300 var 1996 Stålmarck 1000 var 2001 Chaff 10k var
12 SAT (2) 1996 GRASP: ( ) 2001 Chaff: 2005 Minisat: SAT 2005 competition 3 industrial category (industrial )
13 SAT SAT CNF CNF = Conjunctive Normal Form ::= ::= CNF ::= (equi-satisfiable) CNF [Tseitin68]
14 Tseitin encoding ) [a b] [c] (c a b) c [c] c a c b c a b CNF
15 SAT : ( ) (Unit Propagation) P=true P=false : P Q R P=false, R=true Q=true Q=false Q false (= M φ M )
16 SAT : P=true P=false P P Those who do not learn from their mistakes are doomed to repeat them
17 Conflict-driven Clause Learning (CDCL) ( ) ( ) : P=true,Q=false,R=false P Q R (resolution) C ( C) (Non-chronological backtracking) ( )
18 CDCL How a CDCL SAT solver works
19 ( ) ( ) CNF XOR etc.
20 Minisat (C++), picosat (C), SAT4J (Java) Google Optimization Tools SAT Lingeling, glueminisat, CryptoMiniSat, pure Haskell SAT toysat ( toysolver )
21 : toysat p cnf x159 x234 x197 $ toysat UF /uf cnf c #vars 250 c #constraints 1065 c Solving starts... c ============================[ Search Statistics ]============================ c Time Restart Decision Conflict LEARNT Fixed Removed c Limit GC Var Constra c ============================================================================= c 0.0s c 0.0s c 0.1s c 0.1s c 0.1s c 0.2s c 0.4s c 0.6s c 1.1s c 1.6s c 2.3s c 3.3s c 3.4s c 4.0s c #cpu_time = 3.872s c #wall_clock_time = 3.957s c #decision = c #random_decision = 105 c #conflict = c #restart = 11 s SATISFIABLE v v v v x1=false, x2=false, x3=true,
22 : Minisat (Emscripten Javascript ) minisat_emscripten_sudoku/index.html
23 Satisfiability Modulo Theories (SMT)
24 SAT SMT SAT SAT SAT SMT
25 SMT = SAT + SAT SAT ( : a 2 a 0)
26 SMT : a>0 b-2c 0, (a > 0) b=c, (a > 0) c a, b<c c a UNSAT SAT a>0 b-2c 0 b=c c a (b<c) {a>0, b- 2c 0, b=c, c a} Boolean abstraction P=Q=R=S=true T=false P Q R S P Q, P R, P S, T S SAT SAT UNSAT
27 SMT : DPLL(T) (Lazy SMT) DPLL(T) SAT SAT SAT SAT : a = 0, a > 0 P, Q P true Q false
28 ( ) SMT SAT (theory) : ( ) / / ( :, +, read, 3.0)
29 SMT (e.g., +, read) ( ) : x. 0 s(x) x1, x2. s(x1)=s(x2) x1=x2, a,b. a+s(b)=s(a+b)
30 SMT ( ) (List ::= Nil Cons A List) SQL
31 : EUF EUF (Equality and Uninterpreted Function) : ( ) f(b) = c f(c) = a g(a) = h(a,a) (g(b) = h(c,b)) b = c? : Union-Find Congruence Closure
32 (set-logic QF_UF) (set-option :produce-models true) (declare-sort U 0) (declare-fun f (U) U) (declare-fun g (U) U) (declare-fun h (U U) U) (declare-fun a () U) (declare-fun b () U) (declare-fun c () U) (assert (= (f b) c)) (assert (= (f c) a)) (assert (= (g b) (h a a))) (assert (not (= (g b) (h c b)))) (check-sat) (get-model) (assert (= b c)) (check-sat) $ cvc4 --incremental test.smt2 sat (model ; cardinality of U is 5 (declare-sort U 0) ; ; ; ; ; (define-fun f ((_ufmt_1 U)) U (ite _ufmt_1) (define-fun g ((_ufmt_1 U)) (define-fun h ((_ufmt_1 U) (_ufmt_2 U)) U (ite _ufmt_1) (ite (define-fun a () (define-fun b () (define-fun c () ) unsat
33 : Linear Real Arithmetics (LRA) ( ) ( w/o ) :, Fourier-Motzkin, Virtual Substitution Linear Integer Arithmetics (LIA) ( w/o ) : +B&B+, Omega test, Cooper Non-linear Real Arithmetics (NRA) ( w/o ) : Cylindrical Algebraic Decomposision, Virtual Substitution, Gröbner Basis Non-linear Integer Arithmetics (NIA) ( ) [Matiyasevich70]
34 (set-logic QF_AUFLIRA) (set-option :produce-models true) (declare-fun x1 () Real) (declare-fun x2 () Real) (declare-fun x3 () Real) (declare-fun x4 () Int) (assert (<= (+ (- x1) x2 x3 (* 10.0 x4)) 20.0)) (assert (<= (+ x1 (- (* 3.0 x2)) x3) 30.0)) (assert (= (+ x2 (- (* 3.5 x4))) 0.0)) (assert (<= 0.0 x1)) (assert (<= x1 40.0)) (assert (<= 0.0 x2)) (assert (<= 0.0 x3)) (assert (<= 2 x4)) (assert (<= x4 3)) (check-sat) (get-model) $ cvc4 --incremental \ test2.smt2 sat (model (define-fun x1 () Real 7) (define-fun x2 () Real 7) (define-fun x3 () Real 0) (define-fun x4 () Int 2) ) $
35 SMT ( ) SAT 3. C (= C ) SAT 4. ( ) SAT 5. ( )
36 SMT Z3 (Microsoft Research) CVC4 (NYU and U Iowa) Z3 yices (SRI) Z3 MathSAT Boolector OpenSMT ( ) toysat SAT
37 Satisfiability Modulo Theories (SMT)
38 Theory Combination T1, T2 (EUF LIA): 2a b + f(g(c)) f(b) = c f(c) = a g(a) < h(a, a) g(b) > h(c, b) b = c T1 T2 T1 T2?
39 Theory Combination (T1 T2)- 1 2 T1-1 T ( ) : T- T - 1, 2 T1-,T2-1 2 (T1 T2)-
40 Craig interpolation theorem 1 2 1, , SMT T1, T2 1 2 ( )
41 Theory Combination R R A R = (s,t) R (s=t) (s,t) R (s t) A R 1 A R 2 R T 1, T 2 stably-infinite T stably-infinite : T- T-
42 Stably-infiniteness T stably-infinite: T- T- - (Löwenheim Skolem theorem) T1, T2 Stably infinite
43 Nelson-Oppan Theory Combination T1 1 i e i T2 e i ( ) T2 T1
44 Convexity T (convex) : T e i iff ( T e i for some i) T Nelson-Oppan e i e i : EUF, LRA LIA, BV, A LIA = (y=1 z=2 1 x 2) T (x=y x=z) T x=y T x=z
45 TheoryCombination Delayed Theory Combination (DTC) SAT Model-based Theory Combination
46
47 SAT/SMT VC (Verification Condition) ) Isabelle SledgeHammer
48 SAT RCF PBS PBO SMT SAT Max SAT Finite Model Finding QBF
49 Handbook of Satisfiability A. Biere, M. Heule, H. Van Maaren, and T. Walsh, Eds. IOS Press, Feb SAT
50 : SAT,, Vol. 25, No.1 (2010) SAT,", vol. 32, no. 1, pp , /1/32_1_103/_article/-char/en/
51 SMT TPP2011 TPPmark Uniform Candy Distribution SMT Z3
( ) P, P P, P (negation, NOT) P ( ) P, Q, P Q, P Q 3, P Q (logical product, AND) P Q ( ) P, Q, P Q, P Q, P Q (logical sum, OR) P Q ( ) P, Q, P Q, ( P
Advent Calendar 2018 @Fukuso Sutaro,,, ( ) Davidson, 5, 1 (quantification) (open sentence) 1,,,,,, 1 1 (propositional logic) (truth value) (proposition) (sentence) 2 (2-valued logic) 2, true false (truth
[20] CSP CSP CSP SAT CSP SAT SAT SAT SAT SAT [6] SAT [2] SAT SAT [13] [11] CSP SAT Race SAT API API Java 2 1. SAT Race 2015 SAT API Java API 2.
![[20] CSP CSP CSP SAT CSP SAT SAT SAT SAT SAT [6] SAT [2] SAT SAT [13] [11] CSP SAT Race SAT API API Java 2 1. SAT Race 2015 SAT API Java API 2.](/thumbs/92/110929471.jpg "[20] CSP CSP CSP SAT CSP SAT SAT SAT SAT SAT [6] SAT [2] SAT SAT [13] [11] CSP SAT Race SAT API API Java 2 1. SAT Race 2015 SAT API Java API 2.")
32 (2015 ) isugar : SAT SAT (SAT) SAT SAT SAT SAT SAT SAT SAT Race 2015 SAT API SAT API SAT isugar isugar SAT N-iSugar Remarkable improvements on SAT solvers over the last decade have led the success of
パズルをSugar制約ソルバーで解く
Sugar 1 2 3 1 CSPSAT 2008 8 21 Sugar 1 2 3 Sugar Sugar (CSP) (SAT ) (encode) SAT SAT order encoding direct encoding support encoding http://bachistckobe-uacjp/sugar/ Web Sugar 1 2 3 Sugar SAT (COP) MAX-CSP
Bulletin of JSSAC(2014) Vol. 20, No. 2, pp (Received 2013/11/27 Revised 2014/3/27 Accepted 2014/5/26) It is known that some of number puzzles ca
Bulletin of JSSAC(2014) Vol. 20, No. 2, pp. 3-22 (Received 2013/11/27 Revised 2014/3/27 Accepted 2014/5/26) It is known that some of number puzzles can be solved by using Gröbner bases. In this paper,
1 n 1 1 2 2 3 3 3.1............................ 3 3.2............................. 6 3.2.1.............. 6 3.2.2................. 7 3.2.3........................... 10 4 11 4.1..........................
1. A0 A B A0 A : A1,...,A5 B : B1,...,B12 2. 5 3. 4. 5. A0 (1) A, B A B f K K A ϕ 1, ϕ 2 f ϕ 1 = f ϕ 2 ϕ 1 = ϕ 2 (2) N A 1, A 2, A 3,... N A n X N n X N, A n N n=1 1 A1 d (d 2) A (, k A k = O), A O. f
A5 PDF.pwd
Average Treatment Effect; ATE attributes Randomized Factorial Survey Experiment; RFSE cues ATE ATE Hainmueller et al. 2014 Average Marginal Component Effect ATE 67 4 2017 2 845 , ;, ATE, ;, ;, W 846 67
19 Systematization of Problem Solving Strategy in High School Mathematics for Improving Metacognitive Ability
19 Systematization of Problem Solving Strategy in High School Mathematics for Improving Metacognitive Ability 1105402 2008 2 4 2,, i Abstract Systematization of Problem Solving Strategy in High School
2 1/2 1/4 x 1 x 2 x 1, x 2 9 3x 1 + 2x 2 9 (1.1) 1/3 RDA 1 15 x /4 RDA 1 6 x /6 1 x 1 3 x 2 15 x (1.2) (1.3) (1.4) 1 2 (1.5) x 1
1 1 [1] 1.1 1.1. TS 9 1/3 RDA 1/4 RDA 1 1/2 1/4 50 65 3 2 1/15 RDA 2/15 RDA 1/6 RDA 1 1/6 1 1960 2 1/2 1/4 x 1 x 2 x 1, x 2 9 3x 1 + 2x 2 9 (1.1) 1/3 RDA 1 15 x 1 + 2 1/4 RDA 1 6 x 1 1 4 1 1/6 1 x 1 3
「計算と論理」 Software Foundations その4
Software Foundations 4 cal17@fos.kuis.kyoto-u.ac.jp http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal/ November 7, 2017 ( ) ( 4) November 7, 2017 1 / 51 Poly.v ( ) ( 4) November 7, 2017 2 / 51 : (
22 2016 3 82 1 1
: 81 1 2 3 4 1990 2015 22 2016 3 82 1 1 83 : 2 5 84 22 2016 3 6 3 7 8 2 : 85 1 S 12 S S S S S S S S S 86 22 2016 3 S S S S S S S S 2 S S : 87 S 9 3 2 1 10 S 11 22 2016 3 88 1 : 89 1 2 3 4 90 22 2016 3
Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx.
![Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx.](/thumbs/93/111616248.jpg "Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx.")
1, 2 1 m110057@shibaura-it.ac.jp 2 sasano@sic.shibaura-it.ac.jp Eclipse Visual Studio ML Standard ML Emacs 1 ( IDE ) IDE C C++ Java IDE IDE IDE IDE Eclipse Java IDE Java Standard ML 1 print (Int. 1 Int
,.,. NP,., ,.,,.,.,,, (PCA)...,,. Tipping and Bishop (1999) PCA. (PPCA)., (Ilin and Raiko, 2010). PPCA EM., , tatsukaw
,.,. NP,.,. 1 1.1.,.,,.,.,,,. 2. 1.1.1 (PCA)...,,. Tipping and Bishop (1999) PCA. (PPCA)., (Ilin and Raiko, 2010). PPCA EM., 152-8552 2-12-1, tatsukawa.m.aa@m.titech.ac.jp, 190-8562 10-3, mirai@ism.ac.jp
., White-Box, White-Box. White-Box.,, White-Box., Maple [11], 2. 1, QE, QE, 1 Redlog [7], QEPCAD [9], SyNRAC [8] 3 QE., 2 Brown White-Box. 3 White-Box
![., White-Box, White-Box. White-Box.,, White-Box., Maple [11], 2. 1, QE, QE, 1 Redlog [7], QEPCAD [9], SyNRAC [8] 3 QE., 2 Brown White-Box. 3 White-Box](/thumbs/91/105919953.jpg "., White-Box, White-Box. White-Box.,, White-Box., Maple [11], 2. 1, QE, QE, 1 Redlog [7], QEPCAD [9], SyNRAC [8] 3 QE., 2 Brown White-Box. 3 White-Box")
White-Box Takayuki Kunihiro Graduate School of Pure and Applied Sciences, University of Tsukuba Hidenao Iwane ( ) / Fujitsu Laboratories Ltd. / National Institute of Informatics. Yumi Wada Graduate School
1 IDC Wo rldwide Business Analytics Technology and Services 2013-2017 Forecast 2 24 http://www.soumu.go.jp/johotsusintokei/whitepaper/ja/h24/pdf/n2010000.pdf 3 Manyika, J., Chui, M., Brown, B., Bughin,
2 22006 2 e-learning e e 2003 1 4 e e e-learning 2 Web e-leaning 2004 2005 2006 e 4 GP 4 e-learning e-learning e-learning e LMS LMS Internet Navigware
2 2 Journal of Multimedia Aided Education Research 2006, Vol. 2, No. 2, 19 e 1 1 2 2 1 1 GP e 2004 e-learning 2004 e-learning 2005 e-learning e-learning e-learning e-learning 2004 e-learning HuWeb 2005
f(x) x S (optimal solution) f(x ) (optimal value) f(x) (1) 3 GLPK glpsol -m -d -m glpsol -h -m -d -o -y --simplex ( ) --interior --min --max --check -
GLPK by GLPK http://mukun mmg.at.infoseek.co.jp/mmg/glpk/ 17 7 5 : update 1 GLPK GNU Linear Programming Kit GNU LP/MIP ILOG AMPL(A Mathematical Programming Language) 1. 2. 3. 2 (optimization problem) X
Parametric Polymorphism
ML 2 2011/04/19 Parametric Polymorphism Type Polymorphism ? : val hd_int : int list - > int val hd_bool : bool list - > bool val hd_i_x_b : (int * bool) list - > int * bool etc. let hd_int = function (x
IP Management Within Universities: Experiences in the US
yuko.harayama@most.tohoku.ac.jp 17/3/2004 1 Ref. Sandelin TLO expertise Ref. AUTM 17/3/2004 2 Ref. Heller & Eisenberg, 1998 The scientific commons is becoming privatized! (Ref. Nelson, 2003) 17/3/2004
p *2 DSGEDynamic Stochastic General Equilibrium New Keynesian *2 2
2013 1 nabe@ier.hit-u.ac.jp 2013 4 11 Jorgenson Tobin q : Hayashi s Theorem : Jordan : 1 investment 1 2 3 4 5 6 7 8 *1 *1 93SNA 1 p.180 1936 100 1970 *2 DSGEDynamic Stochastic General Equilibrium New Keynesian
n 2 n (Dynamic Programming : DP) (Genetic Algorithm : GA) 2 i
15 Comparison and Evaluation of Dynamic Programming and Genetic Algorithm for a Knapsack Problem 1040277 2004 2 25 n 2 n (Dynamic Programming : DP) (Genetic Algorithm : GA) 2 i Abstract Comparison and
はじめに
IT 1 NPO (IPEC) 55.7 29.5 Web TOEIC Nice to meet you. How are you doing? 1 type (2002 5 )66 15 1 IT Java (IZUMA, Tsuyuki) James Robinson James James James Oh, YOU are Tsuyuki! Finally, huh? What's going
1 [1, 2, 3, 4, 5, 8, 9, 10, 12, 15] The Boston Public Schools system, BPS (Deferred Acceptance system, DA) (Top Trading Cycles system, TTC) cf. [13] [
![1 [1, 2, 3, 4, 5, 8, 9, 10, 12, 15] The Boston Public Schools system, BPS (Deferred Acceptance system, DA) (Top Trading Cycles system, TTC) cf. [13] [](/thumbs/91/106628466.jpg "1 [1, 2, 3, 4, 5, 8, 9, 10, 12, 15] The Boston Public Schools system, BPS (Deferred Acceptance system, DA) (Top Trading Cycles system, TTC) cf. [13] [")
Vol.2, No.x, April 2015, pp.xx-xx ISSN xxxx-xxxx 2015 4 30 2015 5 25 253-8550 1100 Tel 0467-53-2111( ) Fax 0467-54-3734 http://www.bunkyo.ac.jp/faculty/business/ 1 [1, 2, 3, 4, 5, 8, 9, 10, 12, 15] The
2) TA Hercules CAA 5 [6], [7] CAA BOSS [8] 2. C II C. ( 1 ) C. ( 2 ). ( 3 ) 100. ( 4 ) () HTML NFS Hercules ( )
![2) TA Hercules CAA 5 [6], [7] CAA BOSS [8] 2. C II C. ( 1 ) C. ( 2 ). ( 3 ) 100. ( 4 ) () HTML NFS Hercules ( )](/thumbs/78/78162263.jpg "2) TA Hercules CAA 5 [6], [7] CAA BOSS [8] 2. C II C. ( 1 ) C. ( 2 ). ( 3 ) 100. ( 4 ) () HTML NFS Hercules ( )")
1,a) 2 4 WC C WC C Grading Student programs for visualizing progress in classroom Naito Hiroshi 1,a) Saito Takashi 2 Abstract: To grade student programs in Computer-Aided Assessment system, we propose
Akito Tsuboi June 22, T ϕ T M M ϕ M M ϕ T ϕ 2 Definition 1 X, Y, Z,... 1
Akito Tsuboi June 22, 2006 1 T ϕ T M M ϕ M M ϕ T ϕ 2 Definition 1 X, Y, Z,... 1 1. X, Y, Z,... 2. A, B (A), (A) (B), (A) (B), (A) (B) Exercise 2 1. (X) (Y ) 2. ((X) (Y )) (Z) 3. (((X) (Y )) (Z)) Exercise
ON STRENGTH AND DEFORMATION OF REINFORCED CONCRETE SHEAR WALLS By Shigeru Mochizuki Concrete Journal, Vol. 18, No. 4, April 1980, pp. 1 `13 Synopsis A
ON STRENGTH AND DEFORMATION OF REINFORCED CONCRETE SHEAR WALLS By Shigeru Mochizuki Concrete Journal, Vol. 18, No. 4, April 1980, pp. 1 `13 Synopsis After Tokachioki Earthquake of 1968, the importance
設計現場からの課題抽出と提言 なぜ開発は遅れるか？その解決策は？
Work in Progress - Do not publish STRJ WS: March 4, 2004, WG1 1 WG1: NEC STARC STARC Work in Progress - Do not publish STRJ WS: March 4, 2004, WG1 2 WG1 ITRS Design System Drivers SoC EDA Work in Progress
SCM (v0201) ( ) SCM 2 SCM 3 SCM SCM 2.1 SCM SCM SCM (1) MS-DOS (2) Microsoft(R) Windows 95 (C)Copyright Microsoft Corp
SCM (v0201) ( ) 14 4 20 1 SCM 2 SCM 3 SCM 4 5 2 SCM 2.1 SCM SCM 2 1 2 SCM (1) MS-DOS (2) Microsoft(R) Windows 95 (C)Copyright Microsoft Corp 1981-1996. 1 (3) C:\WINDOWS>cd.. C:\>cd scm C:\SCM> C:\SCM>
【教】⑥久我直人先生【本文】／【教】⑥久我直人先生【本文】
Schön Schön Shulman Wilson transformation pedagogical content knowledge Schön Schön Schön Shulman Wilson pedagogical content knowledge Schön Schön Shulman Wilson pedagogical content knowledge Schön Shulman
& 3 3 ' ' (., (Pixel), (Light Intensity) (Random Variable). (Joint Probability). V., V = {,,, V }. i x i x = (x, x,, x V ) T. x i i (State Variable),
.... Deeping and Expansion of Large-Scale Random Fields and Probabilistic Image Processing Kazuyuki Tanaka The mathematical frameworks of probabilistic image processing are formulated by means of Markov
SAT¥½¥ë¥Ð¡¼¤ÎºÇ¿·Æ°¸þ¤ÈÍøÍѵ»½Ñ
SAT web, web 19 PPL2017 2017 3 9 @ 1 / 49 SAT, SAT, SAT,, SAT SAT SAT DPLL, CDCL, SAT, SAT SAT Certified UNSAT, UNSAT, SAT, CEGAR SAT 2 / 49 SAT, SAT, SAT,, SAT SAT SAT DPLL, CDCL, SAT, SAT SAT Certified
TF-IDF TDF-IDF TDF-IDF Extracting Impression of Sightseeing Spots from Blogs for Supporting Selection of Spots to Visit in Travel Sat
1 1 2 1. TF-IDF TDF-IDF TDF-IDF. 3 18 6 Extracting Impression of Sightseeing Spots from Blogs for Supporting Selection of Spots to Visit in Travel Satoshi Date, 1 Teruaki Kitasuka, 1 Tsuyoshi Itokawa 2
1 2 1 2012 39 1964 1997 1 p. 65 1 88 2 1 2 2 1 2 5 3 2 1 89 1 2012 Frantzen & Magnan 2005 2010 6 N2 2014 3 3.1 2015 2009 1 2 3 2 90 2 3 2 B1 B1 1 2 1 2 1 2 1 3.2 1 2014 2015 2 2 2014 2015 9 4.1 91 1 2
å‰Łçı—訋çfl»æ³Łã†¨ã…Łã‡£ã…œã…−ã……ã…†æŁ°, ㆚ㆮ2æ¬¡è©Łä¾¡å‹ƒå›²ã•† ㅋㅪㅜã…−ã……ã…†æŁ°å‹Šã†«ã‡‹ã‡‰é•£ã†®ç¢ºç”⁄訋箊
, 2 August 28 (Fri), 2016 August 28 (Fri), 2016 1 / 64 Outline 1 2 3 2 4 2 5 6 August 28 (Fri), 2016 2 / 64 fibonacci Lucas 2 August 28 (Fri), 2016 3 / 64 Dynamic Programming R.Bellman Bellman Continuum
_01野口.indd
: NPO 83 4 2015 3 1. 1998 NPO NPO NPO NPO NPO 2.NPO 1 NPO 2007 12 2011 4 NPO NPO 2011 3 11 NPO NPO NPO 1 1998 NPO NPO 2 2 NPO NPO NPO NPO 3 83 4 1NPO NPO NPO https://www.npo - homepage.go.jp/portalsite/syokatsutyobetsu_ninshou.html12
FC.. a b b endogenous process of development exogenous factors in change Parsons and Shils,
Roles of Exogenous Factors in Endogenous Regional Development : A Case of Sagano Gabai Bachan Location Shooting Assistance Program in Takeo City Akinori (Aki) Nakamura, Ritsumeikan University Daiki Maeno,
258 5) GPS 1 GPS 6) GPS DP 7) 8) 10) GPS GPS 2 3 4 5 2. 2.1 3 1) GPS Global Positioning System
Vol. 52 No. 1 257 268 (Jan. 2011) 1 2, 1 1 measurement. In this paper, a dynamic road map making system is proposed. The proposition system uses probe-cars which has an in-vehicle camera and a GPS receiver.
untitled
c 645 2 1. GM 1959 Lindsey [1] 1960 Howard [2] Howard 1 25 (Markov Decision Process) 3 3 2 3 +1=25 9 Bellman [3] 1 Bellman 1 k 980 8576 27 1 015 0055 84 4 1977 D Esopo and Lefkowitz [4] 1 (SI) Cover and
【教】⑤吉井健治先生【本文】／【教】⑤吉井健治先生【本文】
Stern, D.N., McWilliams, N., Sullivan, H.S., Kohut, H., Kohut, H. How does analysis cure? The University of Chicago Press. McWilliams, N. Psychoanalytic Case Formulation. Guilford Press. Stern, D.N. The
Vol. 48 No. 3 Mar PM PM PMBOK PM PM PM PM PM A Proposal and Its Demonstration of Developing System for Project Managers through University-Indus
Vol. 48 No. 3 Mar. 2007 PM PM PMBOK PM PM PM PM PM A Proposal and Its Demonstration of Developing System for Project Managers through University-Industry Collaboration Yoshiaki Matsuzawa and Hajime Ohiwa
-2-
-1- -2- -3- -4- -5- -6- -7- -8- 10-9- -10-1 2 -11-1 1-12- -13- -14- Plan Do Check Action Check Action 1 -15- -16- -17- -18- -19- -20- -21- -22- 10 2 9 3 9 2 1 10 2 9 3 6 4 1 6 6 10 2 10 2 11 1 8 1 8 4
149 (Newell [5]) Newell [5], [1], [1], [11] Li,Ryu, and Song [2], [11] Li,Ryu, and Song [2], [1] 1) 2) ( ) ( ) 3) T : 2 a : 3 a 1 :
![149 (Newell [5]) Newell [5], [1], [1], [11] Li,Ryu, and Song [2], [11] Li,Ryu, and Song [2], [1] 1) 2) ( ) ( ) 3) T : 2 a : 3 a 1 :](/thumbs/92/109497872.jpg "149 (Newell [5]) Newell [5], [1], [1], [11] Li,Ryu, and Song [2], [11] Li,Ryu, and Song [2], [1] 1) 2) ( ) ( ) 3) T : 2 a : 3 a 1 :")
Transactions of the Operations Research Society of Japan Vol. 58, 215, pp. 148 165 c ( 215 1 2 ; 215 9 3 ) 1) 2) :,,,,, 1. [9] 3 12 Darroch,Newell, and Morris [1] Mcneil [3] Miller [4] Newell [5, 6], [1]
3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B
![3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B](/thumbs/102/156825138.jpg "3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B")
3 3.1 algebraic datatype data 1 2... k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] Bob String y Charlie Foo Double Integer Alice 3.14 [1,2],
平成20年度内部評価実施結果報告書《本編》
10 11 12 13 14 15 16 17 Plan Do Check Action 1 2 3 4 146 13 20 43 44 45 62 104 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
untitled
1 1 2 3 2 1 ( 0) 2000 00 3 4 Check Action Do Plan 5 6 14001 5000 5000 1000 1000 7 8 9 10 2004 0.1 0.1 0.0 0.0 0.0 15.3 483.5 0.4 11 12 13 14 http://kankyou.pref.shizuoka.jp/seikan/seikanindex.htm 15 16
NLC配布用.ppt
Semantic Web September 20, 200 IBM( ) (uramoto@jp.ibm.com) Semantic Web ( )? Semantic Web 2 What can it do? (by Jim Hendler) 3 Semantic Web W3C Director Berners-Lee Web The Semantic Web is an extension
ブック
ARMA Estimation on Process of ARMA Time Series Model Sanno University Bulletin Vol.26 No. 2 February 2006 ARMA Estimation on Process of ARMA Time Series Model Many papers and books have been published
Mathematical Logic I 12 Contents I Zorn
Mathematical Logic I 12 Contents I 2 1 3 1.1............................. 3 1.2.......................... 5 1.3 Zorn.................. 5 2 6 2.1.............................. 6 2.2..............................
ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1
2005 sumii@ecei.tohoku.ac.jp 2005 6 24 ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1 let λ 1 let x = e1 in e2 (λx.e 2 )e 1 e 1 x e 2 λ 3 λx.(λy.e)
1 1,200m ,482,620m 1 323,825m 1 205,988m 114,988m 60,000m 31,000m ,837m ,158,795m ,340m 1 48,006m 1 33,016m 1,125m
IV 39 7 10 167 1 3 9 2 10 79 1 1,200m 23 23 6 1 429 2,482,620m 1 323,825m 1 205,988m 114,988m 60,000m 31,000m 27 117,837m 3 2 426 2,158,795m 44 277,340m 1 48,006m 1 33,016m 1,125m 33,016m 4 14,990m 2 44
3675-433897418-1.pdf
A : : : : : : : : : : PR PR NHK 2 PR PR 3 1954 7 4 5 9 12,000 12 100 2 2 11 4 5 6 7 / PR 8 9 10 11 1952 ( ) 2008 2009 2012 NHK km m m 12 m km km kg kg 13 % 14 15 1959 5 20 8 17100kg 400kg How much? 60
joho09.ppt
s M B e E s: (+ or -) M: B: (=2) e: E: ax 2 + bx + c = 0 y = ax 2 + bx + c x a, b y +/- [a, b] a, b y (a+b) / 2 1-2 1-3 x 1 A a, b y 1. 2. a, b 3. for Loop (b-a)/ 4. y=a*x*x + b*x + c 5. y==0.0 y (y2)
28_3-03-伊勢坊 中原先生-原著③.indd
Japanese Journal of Administrative Science Volume 28, No.3, 2016, 233-247 Article How do executive secretaries learn from their experiences? Aya ISEBO Tokyo University Jun NAKAHARA Tokyo University The
Java equals hashcode
Java equals hashcode 26 2 5 25 Java equals hashcode Java equals hashcode ( equals Java Alloy Alloy Analyzer equals hashcode hashcode equals hashcode equals Java equals hashcode Alloy Analyzer SAT hashcode
kubostat2018d p.2 :? bod size x and fertilization f change seed number? : a statistical model for this example? i response variable seed number : { i
kubostat2018d p.1 I 2018 (d) model selection and kubo@ees.hokudai.ac.jp http://goo.gl/76c4i 2018 06 25 : 2018 06 21 17:45 1 2 3 4 :? AIC : deviance model selection misunderstanding kubostat2018d (http://goo.gl/76c4i)
LMS LMS 2014 LMS 2 Moodle 2. LMS LMS e-learning Web LMS MOOC Moodle LMS ( 1 ) ( 2 ) ( 3 ) 24 ( 4 ) ( 5 ) ( 6 ) 1 LMS Web CS LMS Instructu
LMS 1 2 2 LMS Blended-Learning CS PC Web LMS MOOC CS PC LMS LMS Requested Features for Mobile Learning Application dedicated to LMS Toshiyuki Kamada 1 Yasushi Kodama 2 Yuki Terawaki 2 Abstract: The blended-learning
【教】⑩山森直人先生【本文】／【教】⑩山森直人先生【本文】
c.f. pp community of practice c.f. pp c.f. p pp c.f. Hutchins, CD c.f. teacher development surpriseschön, inquiryfreeman, puzzles Allwright, P P P P P P e IC Microsoft Excel KJ P P P P P P ALT ALT T ALT
A Brief Introduction to Modular Forms Computation
A Brief Introduction to Modular Forms Computation Magma Supported by GCOE Program Math-For-Industry Education & Research Hub What s this? Definitions and Properties Demonstration H := H P 1 (Q) some conditions
Basic Math. 1 0 [ N Z Q Q c R C] 1, 2, 3,... natural numbers, N Def.(Definition) N (1) 1 N, (2) n N = n +1 N, (3) N (1), (2), n N n N (element). n/ N.
![Basic Math. 1 0 [ N Z Q Q c R C] 1, 2, 3,... natural numbers, N Def.(Definition) N (1) 1 N, (2) n N = n +1 N, (3) N (1), (2), n N n N (element). n/ N.](/thumbs/93/113887245.jpg "Basic Math. 1 0 [ N Z Q Q c R C] 1, 2, 3,... natural numbers, N Def.(Definition) N (1) 1 N, (2) n N = n +1 N, (3) N (1), (2), n N n N (element). n/ N.")
Basic Mathematics 16 4 16 3-4 (10:40-12:10) 0 1 1 2 2 2 3 (mapping) 5 4 ε-δ (ε-δ Logic) 6 5 (Potency) 9 6 (Equivalence Relation and Order) 13 7 Zorn (Axiom of Choice, Zorn s Lemma) 14 8 (Set and Topology)
koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1
http://www.kb.ecei.tohoku.ac.jp/ koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ 1.1.1 λ, syntax τ (types) ::= b τ 1 τ 2 τ 1 τ 2 M (terms) ::= c τ x M 1 M 2 λx : τ.m (M 1,M 2
1009.\1.\4.ai
- 1 - E O O O O O O - 2 - E O O O - 3 - O N N N N N N N N N N N N N N N N N N N N N N N E e N N N N N N N N N N N N N N N N N N N N N N N D O O O - 4 - O O O O O O O O N N N N N N N N N N N N N N N N N
教育における構成主義
Abstract The idea of constructivism now pervades the educational literature. Constructivism implies that knowledge is always knowledge that a person constructs. It stresses the need to encourage greater
bdd.gby
Haskell Behavior Driven Development 2012.5.27 @kazu_yamamoto 1 Haskell 4 Mew Firemacs Mighty ghc-mod 2 Ruby/Java HackageDB 3 Haskeller 4 Haskeller 5 Q) Haskeller A) 6 7 Haskeller Haskell 8 9 10 Haskell
J No J. J
教育科学と教育実践 2 Science of Education and Educational Practice - A Perspective on the Controversy on the Science of Education in Post-War Japan Part Takeo TANAKA 1950 E. J. E. J. E. J. Abstract In the latter
Fig. 3 Flow diagram of image processing. Black rectangle in the photo indicates the processing area (128 x 32 pixels).
Fig. 1 The scheme of glottal area as a function of time Fig. 3 Flow diagram of image processing. Black rectangle in the photo indicates the processing area (128 x 32 pixels). Fig, 4 Parametric representation
140 120 100 80 60 40 20 0 115 107 102 99 95 97 95 97 98 100 64 72 37 60 50 53 50 36 32 18 H18 H19 H20 H21 H22 H23 H24 H25 H26 H27 1 100 () 80 60 40 20 0 1 19 16 10 11 6 8 9 5 10 35 76 83 73 68 46 44 H11
第1部門_03_北川純子.indd
22 1920 1930 31 37 1980 28 1950 1970 1923-2001 1929-2002 18 10 20 11 1904-1958 1968:344 29 12 13 form 30 14 CD 1899-1964 2008 COCJ35023 2008, COCJ35022 15 = = = 16 31 32 17 2 a1 2 a a2 ( ) 33 18 2007 KICH2445
1980年代半ば，米国中西部のモデル 理論，そして未来－モデル理論賛歌
2016 9 27 RIMS 1 2 3 1983 9-1989 6 University of Illinois at Chicago (UIC) John T Baldwin 1983 9-1989 6 University of Illinois at Chicago (UIC) John T Baldwin Y N Moschovakis, Descriptive Set Theory North
200708_LesHouches_02.ppt
Numerical Methods for Geodynamo Simulation Akira Kageyama Earth Simulator Center, JAMSTEC, Japan Part 2 Geodynamo Simulations in a Sphere or a Spherical Shell Outline 1. Various numerical methods used
gengo.dvi
4 97.52% tri-gram 92.76% 98.49% : Japanese word segmentation by Adaboost using the decision list as the weak learner Hiroyuki Shinnou In this paper, we propose the new method of Japanese word segmentation
A Study on Throw Simulation for Baseball Pitching Machine with Rollers and Its Optimization Shinobu SAKAI*5, Yuichiro KITAGAWA, Ryo KANAI and Juhachi
A Study on Throw Simulation for Baseball Pitching Machine with Rollers and Its Optimization Shinobu SAKAI*5, Yuichiro KITAGAWA, Ryo KANAI and Juhachi ODA Department of Human and Mechanical Systems Engineering,
Solution Report
CGE 3 GAMS * Date: 2018/07/24, Version 1.1 1 2 2 GAMSIDE 3 2.1 GAMS................................. 3 2.2 GAMSIDE................................ 3 2.3 GAMSIDE............................. 7 3 GAMS 11
ab c d 6 12 1:25,000 28 3 2-1-3 18 2-1-10 25000 3120 10 14 15 16 7 2-1-4 1000ha 10100ha 110ha ha ha km 200ha 100m 0.3 ha 100m 1m 2-1-11 2-1-5 20cm 2-1-12 20cm 2003 1 05 12 2-1-13 1968 10 7 1968 7 1897
...v..&.{..&....
8 pp.- 2006 * h ** *** An empirical analysis on the efficiency of the M&A among the non-financial companies based on DEA Hidetoshi KOKUBO*, Koichi MIYAZAKI**, Tomohiko TAKAHASHI*** Abstract Using DEA (Data
情報の構造とデータ処理
mizutani@ic.daito.ac.jp 2014 SQL information system input process output (information) (symbols) (information structure) (data) 201411 ton/kg m/feet km 2 /m 2 (data structure) (integer) (real) (boolean)
Abstract This paper concerns with a method of dynamic image cognition. Our image cognition method has two distinguished features. One is that the imag
2004 RGB A STUDY OF RGB COLOR INFORMATION AND ITS APPLICATION 03R3237 Abstract This paper concerns with a method of dynamic image cognition. Our image cognition method has two distinguished features. One
鹿大広報149号
No.149 Feb/1999 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 Learned From Japanese Life and Experiences in Kagoshima When I first came to Japan I was really surprised by almost everything, the weather,
1 = = = (set) (element) a A a A a A a A a A {2, 5, (0, 1)}, [ 1, 1] = {x; 1 x 1}. (proposition) A = {x; P (x)} P (x) x x a A a A Remark. (i) {2, 0, 0,
![1 = = = (set) (element) a A a A a A a A a A {2, 5, (0, 1)}, [ 1, 1] = {x; 1 x 1}. (proposition) A = {x; P (x)} P (x) x x a A a A Remark. (i) {2, 0, 0,](/thumbs/91/105754557.jpg "1 = = = (set) (element) a A a A a A a A a A {2, 5, (0, 1)}, [ 1, 1] = {x; 1 x 1}. (proposition) A = {x; P (x)} P (x) x x a A a A Remark. (i) {2, 0, 0,")
2005 4 1 1 2 2 6 3 8 4 11 5 14 6 18 7 20 8 22 9 24 10 26 11 27 http://matcmadison.edu/alehnen/weblogic/logset.htm 1 1 = = = (set) (element) a A a A a A a A a A {2, 5, (0, 1)}, [ 1, 1] = {x; 1 x 1}. (proposition)
Vol. 48 No. 4 Apr LAN TCP/IP LAN TCP/IP 1 PC TCP/IP 1 PC User-mode Linux 12 Development of a System to Visualize Computer Network Behavior for L
Vol. 48 No. 4 Apr. 2007 LAN TCP/IP LAN TCP/IP 1 PC TCP/IP 1 PC User-mode Linux 12 Development of a System to Visualize Computer Network Behavior for Learning to Associate LAN Construction Skills with TCP/IP
130 Oct Radial Basis Function RBF Efficient Market Hypothesis Fama ) 4) 1 Fig. 1 Utility function. 2 Fig. 2 Value function. (1) (2)
Vol. 47 No. SIG 14(TOM 15) Oct. 2006 RBF 2 Effect of Stock Investor Agent According to Framing Effect to Stock Exchange in Artificial Stock Market Zhai Fei, Shen Kan, Yusuke Namikawa and Eisuke Kita Several
Jacques Garrigue
Jacques Garrigue Garrigue 1 Garrigue 2 $ print_lines () > for i in $1; do > echo $i > done $ print_lines "a b c" a b c Garrigue 3 Emacs Lisp (defun print-lines (lines) (dolist (str lines) (insert str)
Building a Culture of Self- Access Learning at a Japanese University An Action Research Project Clair Taylor Gerald Talandis Jr. Michael Stout Keiko Omura Problem Action Research English Central Spring,
# let st1 = {name = "Taro Yamada"; id = };; val st1 : student = {name="taro Yamada"; id=123456} { 1 = 1 ;...; n = n } # let string_of_student {n
II 6 / : 2001 11 21 (OCaml ) 1 (field) name id type # type student = {name : string; id : int};; type student = { name : string; id : int; } student {} type = { 1 : 1 ;...; n : n } { 1 = 1 ;...; n = n
FA FA FA FA FA 5 FA FA 9
30 29 31 1993 2004 The process of the labor negotiations of Japan Professional Baseball Players Association, 1993 2004 ABE Takeru Graduate School of Social Science, Hitotsubashi University Abstract The
Web Web [4] Web Web [5] Web 2 Web 3 4 Web Web 2.1 Web Web Web Web Web 2.2 Web Web Web *1 Web * 2*3 Web 3. [6] [7] [8] 4. Web 4.1 Web Web *1 Ama
![Web Web [4] Web Web [5] Web 2 Web 3 4 Web Web 2.1 Web Web Web Web Web 2.2 Web Web Web *1 Web * 2*3 Web 3. [6] [7] [8] 4. Web 4.1 Web Web *1 Ama](/thumbs/84/90061492.jpg "Web Web [4] Web Web [5] Web 2 Web 3 4 Web Web 2.1 Web Web Web Web Web 2.2 Web Web Web *1 Web * 2*3 Web 3. [6] [7] [8] 4. Web 4.1 Web Web *1 Ama")
1 2 2 3 Web Web A product recommender system based on knowledge on situations, functions, and series of products: Implementation and evaluation of the prototype system Abstract: The aim of this study is
1. A0 A B A0 A : A1,...,A5 B : B1,...,B
1. A0 A B A0 A : A1,...,A5 B : B1,...,B12 2. 3. 4. 5. A0 A, B Z Z m, n Z m n m, n A m, n B m=n (1) A, B (2) A B = A B = Z/ π : Z Z/ (3) A B Z/ (4) Z/ A, B (5) f : Z Z f(n) = n f = g π g : Z/ Z A, B (6)
Memetic 26 2 (125T208T)
Memetic 26 2 (125T208T) Abstract The Facility Dispersion Problem(FDP) is compinatorial optimization problem which is selecting facilities to maximize each distance as far as possible in case of selecting
Jorgenson F, L : L: Inada lim F =, lim F L = k L lim F =, lim F L = 2 L F >, F L > 3 F <, F LL < 4 λ >, λf, L = F λ, λl 5 Y = Const a L a < α < CES? C
27 nabe@ier.hit-u.ac.jp 27 4 3 Jorgenson Tobin q : Hayashi s Theorem Jordan Saddle Path. GDP % GDP 2. 3. 4.. Tobin q 2 2. Jorgenson F, L : L: Inada lim F =, lim F L = k L lim F =, lim F L = 2 L F >, F
心理学部紀要 ８号☆／５．東
2014 3 1 8 67 87 2012 Analysis of Voting Behavior on Japanese General Election in 2012 : Using Data of Labor Union Members and the General Voting Public Masanori HIGASHI 2012 61.516.9 2 3 2 8 2009 8 30
評論・社会科学 ８７号（よこ）（Ｐ）／１．小林
! 1 2 1978 1984 3 1984 1992 4 1992 5 1 2007 1 25 2006 GDP 10.7 20 9407 2005 0.3 2006 11 13 2007 9.6 " 1 10 1000 2! 2002 " 3 1 1 1970 1949 1978 4 1978 1984 5 1984 1992 1992 1 1 2 1978 1984 2 1 1978 1984
ISSN NII Technical Report Patent application and industry-university cooperation: Analysis of joint applications for patent in the Universit
ISSN 1346-5597 NII Technical Report Patent application and industry-university cooperation: Analysis of joint applications for patent in the University of Tokyo Morio SHIBAYAMA, Masaharu YANO, Kiminori
/ , ,908 4,196 2, ,842 38, / / 2 33 /
MathWorks Automotive Conference 2014 ( ) ECU 0.1. 1 /30 1949 12 16 1,874 4 959 2 4,908 4,196 2,993 139,842 38,581 62 26 35 56 / 6 185 13 4 3 11 / 2 33 / 2014 3 31 0.1. 2 /30 ETC 0.2. 3 /30 1. 1. 2. 2.
34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., Functional Program Synthesis from Relational Specifica
![34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., Functional Program Synthesis from Relational Specifica](/thumbs/95/122814449.jpg "34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., Functional Program Synthesis from Relational Specifica")
34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., Functional Program Synthesis from Relational Specifications. This is an unrefereed paper. Copyrights belong
( ) (, ) arxiv: hgm OpenXM search. d n A = (a ij ). A i a i Z d, Z d. i a ij > 0. β N 0 A = N 0 a N 0 a n Z A (β; p) = Au=β,u N n 0 A
( ) (, ) arxiv: 1510.02269 hgm OpenXM search. d n A = (a ij ). A i a i Z d, Z d. i a ij > 0. β N 0 A = N 0 a 1 + + N 0 a n Z A (β; p) = Au=β,u N n 0 A-. u! = n i=1 u i!, p u = n i=1 pu i i. Z = Z A Au
Table 1. Reluctance equalization design. Fig. 2. Voltage vector of LSynRM. Fig. 4. Analytical model. Table 2. Specifications of analytical models. Fig
Mover Design and Performance Analysis of Linear Synchronous Reluctance Motor with Multi-flux Barrier Masayuki Sanada, Member, Mitsutoshi Asano, Student Member, Shigeo Morimoto, Member, Yoji Takeda, Member
SEJulyMs更新V7
1 2 ( ) Quantitative Characteristics of Software Process (Is There any Myth, Mystery or Anomaly? No Silver Bullet?) Zenya Koono and Hui Chen A process creates a product. This paper reviews various samples
橡早川ゼミ卒業論文 棟安.PDF
4 1998 J J 3 6 1 J J J J 3 1 1993 1 5 1993 1997 3 3 10 J CP 3 3 CP J 10 300 J 300 J 13 9000 J 2 5 10 25 1978 100 J 1994 pp105106 pp118121 1 J CATEGORY CP 92 10 J CATEGORY 1000 2 CATEGORY J CP CATEGORY
FA
29 28 15 1985 1993 The process of the labor negotiations of the Japan Professional Baseball Players Association, 1985 1993 ABE Takeru Graduate School of Social Science, Hitotsubashi University Abstract