Z3
https://github.com/z3prover/z3
Z3Py チュートリアル
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
$ pip install z3-solver
<この項は書きかけです。順次追記します。>
Z3 in intelliJ IDEA for Mac
https://qiita.com/devdazy/items/8bad17a318fe413b88b8
[Python]Z3で数独パズルを解く
https://qiita.com/fuloru169/items/de8c53402f4998177dfd
[Python]Z3で数独パズルを解くをリファクタリング
https://qiita.com/SatoshiTerasaki/items/bb9f4862ac79cbfa9759
Windows環境でPythonのz3pyを導入する
https://qiita.com/SatoshiTerasaki/items/476c9938479a4bfdda52
自動定理証明でソクラテスは死ぬ The Z3 Theorem Prover(C++)
https://qiita.com/suzukikojiro/items/1f1b82eba672723a0b02
「サイゼリヤで1000円あれば最大何kcal摂れるのか」をSMTソルバー(Z3)で解いてみた。(haskell)
https://qiita.com/tanakh/items/a1fb13f78e0576415de3
F#でZ3
https://qiita.com/minfuk/items/688ddf21c8283a7ca974
Hello SMT-Solver by z3
https://qiita.com/tachiyama/items/2c1dae78ff8104a2b327
How to use Z3 library in Scala with Eclipse
https://qiita.com/quentin-maisonneuve/items/4f32cf52293dc44ffc3d
Z3による汎用大域的最適化
https://qiita.com/kotauchisunsun/items/90bce940a1c08ca1b7ae
Z3によるXORを再現するニューラルネットワークの構築
https://qiita.com/kotauchisunsun/items/d318283fc20df5d25ae7
熊澤 努
GSLetterNeo vol.148 2020 年 11 月
SMT ソルバーZ3 を使った問題解決入門 熊澤 努 kumazawa @ sra.co.jp
1 片山卓
「国民年金法の述語論理による記述と検証 SMT ソルバーZ3Py を用いたケーススタデ ィ」，コンピュータソフトウェア，Vol. 36，No.3，pp. 33-46，2019
https://doi.org/10.11309/jssst.36.3_33
1.1
[ 1 ] 榎並利博:近年の “立法爆発”で法律は “スパゲティ状態”の限界に, 法と経済のジャーナル，http://judiciary.asahi.com/fukabori/2015091500002.html
1.2
[ 2 ] 角田篤泰:ソフトウェア工学との類似性に着目 した立法支援方法 (1)，名古屋大學法政論集，235 号，2010, pp. 41–99. (http://ir.nul.nagoya-u.ac.jp/jspui/handle/2237/14329).
(3)
https://nagoya.repo.nii.ac.jp/record/12874/files/06_kakuta.pdf
[ 3 ] 角田篤泰，島亜紀，齋藤大地，大谷忠:全国自治体 例規データベース eLen の構築と定量的例規調査，情報 ネットワーク・ローレビュー，第 13 巻，第 1 号，(2014), pp. 14–33.
[ 4 ] 片山卓也 (編):法令工学の提案,JAIST Press(2007). [ 5 ] 片山卓也:法律の作成にソフトウェア開発技術を，情報処理 Vol. 58，No. 1，2017, pp. 35.
[ 6 ] 国民年金法, http://www.law.e-gov.go.jp/htmldata/S34/S34HO141.html
[7] 国民年金法逐条解釈(平成27年4月1日現在施行法令準拠)，厚生労働省
8
[ 8 ] Moura, L.:SMT Solvers: Theory and Imple- mentation, Summer School on Logic and The- orem Proving,
https://leodemoura.github.io/files/oregon08.pdf
8.1
[Ack54] W. Ackermann. Solvable cases of the decision problem. Studies in Logic and the Foundation of Mathematics, 1954
8.2
[ABC+02] G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, and R. Sebastiani. A SAT based approach for solving formulas over boolean and linear mathematical propositions. In Proc. of CADE’02, 2002
8.3
[BDS00] C. Barrett, D. Dill, and A. Stump. A framework for cooperating decision procedures. In 17th International Conference on Computer-Aided Deduction, volume 1831 of Lecture Notes in Artificial Intelligence, pages 79–97. Springer-Verlag, 2000
8.4
[BdMS05] C. Barrett, L. de Moura, and A. Stump. SMT-COMP: Satisfiability Modulo Theories Competition. In Int. Conference on Computer Aided Verification (CAV’05), pages 20–23. Springer, 2005
8.5
[BDS02] C. Barrett, D. Dill, and A. Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In Ed Brinksma and Kim Guldstrand Larsen, editors, Proceedings of the 14th International Conference on Computer Aided Verification (CAV ’02), volume 2404 of Lecture Notes in Computer Science, pages 236–249. Springer-Verlag, July 2002. Copenhagen, Denmark
8.6
[BBC+05] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Ranise, and R. Sebastiani. Efficient satisfiability modulo theories via delayed theory combination. In Int. Conf. on Computer-Aided Verification (CAV), volume 3576 of LNCS. Springer, 2005
8.7
[Chv83] V. Chvatal. Linear Programming. W. H. Freeman, 1983
CG96] B. Cherkassky and A. Goldberg. Negative-cycle detection algorithms. In European Symposium on Algorithms, pages 349–363, 1996
8.8
[DLL62] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394–397, July 1962
8.9
[DNS03] D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs, 2003
8.10
[DST80] P. J. Downey, R. Sethi, and R. E. Tarjan. Variations on the Common Subexpression Problem. Journal of the Association for Computing Machinery, 27(4):758–771, 1980
8.11
[dMR02] L. de Moura and H. Rueß. Lemmas on demand for satisfiability solvers. In Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002). Cincinnati, Ohio, 2002
8.12
[DdM06] B. Dutertre and L. de Moura. Integrating simplex with DPLL(T ). Technical report, CSL, SRI International, 2006
8.13
[dMB07b] L. de Moura and N. Bjørner. Efficient E-Matching for SMT solvers. In CADE-21, pages 183–198, 2007
8.14
[dMB07c] L. de Moura and N. Bjørner.
Model Based Theory Combination. In SMT’07, 2007 Relevancy Propagation . Technical Report MSR-TR-2007-140,
8.15
[dMB07a] L. de Moura and N. Bjørner. Microsoft Research, 2007
8.16
[dMB08a]
L. de Moura and N. Bjørner.
Z3: An Efficient SMT Solver. In TACAS 08, 2008
8.17
[dMB08c]
L. de Moura and N. Bjørner.Engineering DPLL(T) + Saturation. In IJCAR’08, 2008
8.18
[dMB08b]
L. de Moura and N. Bjørner. Deciding Effectively Propositional Logic using DPLL and substitution sets. In IJCAR’08, 2008
8.19
[GHN+04] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Int. Conference on Computer Aided Verification (CAV 04), volume 3114 of LNCS, pages 175–188. Springer, 2004
8.20
[MSS96] J. Marques-Silva and K. A. Sakallah. GRASP - A New Search Algorithm for Satisfiability. In Proc. of ICCAD’96, 1996
8.21
[NO79] G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979
8.22
[NO05] R. Nieuwenhuis and A. Oliveras. DPLL(T) with exhaustive theory propagation and its application to difference logic. In Int. Conference on Computer Aided Verification (CAV’05), pages 321–334. Springer, 2005
8.23
[Opp80] D. Oppen. Reasoning about recursively defined data structures. J. ACM, 27(3):403–411, 1980
8.24
[PRSS99] A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small
domains instantiations. Lecture Notes in Computer Science, 1633:455–469, 1999
8.25
[Pug92] William Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Communications of the ACM, volume 8, pages 102–114, August 1992
8.26
[RT03]
S. Ranise and C. Tinelli. The smt-lib format: An initial proposal. In Proceedings of the 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR’03), Miami, Florida, pages 94–111, 2003
8.27
[RS01]
H. Ruess and N. Shankar. Deconstructing shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19–28, June 2001
8.28
[SLB03] S. Seshia, S. Lahiri, and R. Bryant. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In Proc. 40th Design Automation Conference, pages 425–430. ACM Press, 2003
8.29
[Sho81] R. Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769–779, October 1981
9
[ 9 ] Moura, L.:Z3 guide:
http://rise4fun.com/Z3/tutorial/guide
[10] Moura, L.:Z3Py guide:Z3 API in Python, http://cpl0.net/∼argp/papers/z3py-guide.pdf
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
11
[11] Moura, L.:Z3 Advanced Topics, http://www.cs.tau.ac.il/msagiv/courses/asv/z3py/advanced- examples.htm
##12
[12] Moura, L., Bjorner, N.:Proofs and Refutations, and Z3, https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-iwil08.pdf
[1] AaronStumpandDuckkiOe.TowardsanSMTProofFormat.In6’thInternationalWorkshoponSMT,2008.
[2] AlessandroCimatti,AlbertoGriggio,andRobertoSebastiani.EfficientInterpolantGenerationinSatisfiabil-
ity Modulo Theories. In Ramakrishnan and Rehof [15], pages 397–412.
[3] Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Ramakrishnan and Rehof [15].
[4] Leonardo de Moura and Nikolaj Bjørner. Engineering DPLL(T) + Saturation. In IJCAR’08, 2008.
[5] Bruno Dutertre and Leonardo de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In CAV’06, LNCS
4144, pages 81–94. Springer-Verlag, 2006.
[6] NiklasEe ́nandNiklasSo ̈rensson.AnExtensibleSAT-solver.InEnricoGiunchigliaandArmandoTacchella,
editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer, 2003.
[7] Imre Lakatos. Proofs and Refutations. Cambridge University Press, 1976.
[8] Jia Meng and Lawrence C. Paulson. Translating Higher-Order Clauses to First-Order Clauses. J. Autom.
Reasoning, 40(1):35–60, 2008.
[9] Michal Moskal. Rocket-Fast Proof Checking for SMT Solvers. In Ramakrishnan and Rehof [15], pages
486–500.
[10] MatthewW.Moskewicz,ConorF.Madigan,YingZhao,LintaoZhang,andSharadMalik.Chaff:Engineering
an efficient sat solver. In DAC, pages 530–535. ACM, 2001.
[11] Robert Nieuwenhuis and Albert Oliveras. Proof-Producing Congruence Closure. In Ju ̈rgen Giesl, editor,
RTA, volume 3467 of Lecture Notes in Computer Science, pages 453–468. Springer, 2005.
[12] RobertNieuwenhuisandAlbertRubio.Paramodulation-BasedTheoremProving.InRobinsonandVoronkov
[16], pages 371–443.
[13] Roberto Niewenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 53(6):937–977, November 2006.
[14] Andreas Nonnengart and Christoph Weidenbach. Computing small clause normal forms. In Robinson and Voronkov [16], pages 335–367.
[15] C. R. Ramakrishnan and Jakob Rehof, editors. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science. Springer, 2008.
[16] John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001.
[17] S. Schulz. Learning Search Control Knowledge for Equational Theorem Proving. In F. Baader, G. Brewka, and T. Eiter, editors, Proc. of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001), volume 2174 of LNAI, pages 320–334. Springer, 2001.
[18] Aaron Stump, Clark W. Barrett, and David L. Dill. Producing proofs from an arithmetic decision procedure in elliptical lf. Electr. Notes Theor. Comput. Sci., 70(2), 2002.
[19] Aaron Stump and David L. Dill. Faster Proof Checking in the Edinburgh Logical Framework. In Andrei Voronkov, editor, CADE, volume 2392 of Lecture Notes in Computer Science, pages 392–407. Springer, 2002.
[20] GeoffSutcliffe.SemanticDerivationVerification:TechniquesandImplementation.InternationalJournalon Artificial Intelligence Tools, 15(6):1053–1070, 2006.
[21] Tjark Weber and Hasan Amjad. Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic, July 2007.
[22] Yeting Ge and Clark Barrett. Proof Translation and SMT-LIB Benchmark Certification: A Preliminary Report. In 6’th International Workshop on SMT, 2008.
13
[13] 新田克己，長尾順太郎，水鳥哲也:工業所有権法の 知識表現システム KRIP，情報処理学会論文誌 27 巻 11号，pp. 1042–1052 (1986).
14
[14] OCL:Object constraint language 2.0(2006)
http://www.omg.org/spec/OCL/2.2/PDF/
14.1
[AFGP96] A. Artale, E. Franconi, N. Guarino, and L. Pazzi. Part-whole relations in object-centered systems: An overview. Data & Knowledge Engineering, 20(3):347–383, November 1996.
[AHV95] S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. [Akehurst2001] D.H. Akehurst and B. Bordbar, On Querying UML Data Models with OCL, proceedings of the
UML 2001 conference.
[BHSOG01] F. Barbier, B. Henderson-Sellers, A. L. Opdahl, and M. Gogolla. The whole-part relationship in the Unified Modeling Language: A new approach. In K. Siau and T. Halpin, editors, Unified Modeling Language: Systems Analysis, Design and Development Issues, chapter 12, pages 185–209. Idea Publishing Group, 2001.
[BHS99] F. Barbier and B. Henderson-Sellers. Object metamodeling of the whole-part relationship. In C. Mingins, editor, Proceedings of TOOLS Pacific 1999. IEEE Computer Society, 1999.
[CKM+99] S. Cook, A. Kleppe, R. Mitchell, B. Rumpe, J. Warmer, and A. Wills. The Amsterdam manifesto on OCL. Technical Report TUM-I9925, Technische Universit ̈at M ̈unchen, December 1999.
[Clark2000] Tony Clark, Andy Evans, Stuart Kent, Steve Brodsky, Steve Cook, A feasibility Study in Rearchitecting UML as a Family of Languages using a Precise OO Meta-Modeling Approach, version 1.0, September 2000, available from www.puml.org.
[Cla99] T. Clark. Type checking UML static diagrams. In R. France and B. Rumpe, editors, UML’99 - The Unified Modeling Language. Beyond the Standard. Second International Conference, Fort Collins, CO, USA, October 28- 30. 1999, Proceedings, volume 1723 of LNCS, pages 503–517. Springer, 1999.
[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17(4):471–522, December 1985.
[Dat90] C. J. Date. An Introduction to Database Systems – Vol. I. Addison-Wesley, Reading (MA), 1990. [EN94] R. Elmasri and S. B. Navathe. Fundamentals of Database Systems. The Benjamin/Cummings Publishing
Company, Inc., 2 edition, 1994.
[Gog94] M. Gogolla. An Extended Entity-Relationship Model – Fundamentals and Pragmatics, volume 767 of
LNCS. Springer, Berlin, 1994.
[GR99] M. Gogolla and M. Richters. Transformation rules for UML class diagrams. In J. B ́ezivin and P.-A. Muller, editors, The Unified Modeling Language, UML’98 - Beyond the Notation. First International Workshop, Mulhouse, France, June 1998, Selected Papers, volume 1618 of LNCS, pages 92–106. Springer, 1999.
Object Constraint Language, v2.2 219
[Her95] R. Herzig. Zur Spezifikation von Objektgesellschaften mit TROLL light. VDI-Verlag, D ̈usseldorf, Reihe 10 der Fortschritt-Berichte, Nr. 336, 1995. (Dissertation, Naturwissenschaftliche Fakult ̈at, Technische Universit ̈at Braunschweig, 1994).
[HSB99] B. Henderson-Sellers and F. Barbier. Black and white diamonds. In R. France and B. Rumpe, editors, UML’99 - The Unified Modeling Language. Beyond the Standard. Second International Conference, Fort Collins, CO, USA, October 28-30. 1999, Proceedings, volume 1723 of LNCS, pages 550–565. Springer, 1999.
[Kleppe2000] Anneke Kleppe and Jos Warmer, Extending OCL to include Actions, in Andy Evans, Stuart Kent and Bran Selic (editors), <>2000 - The Unified Modeling Language. Advancing the Standard. Third International Conference, York, UK, October 2000, Proceedings, volume 1939 of LNCS. Springer, 2000.
[Kleppe2001] Anneke Kleppe and Jos Warmer, Unification of Static and Dynamic Semantics of UML: a Study in redefining the Semantics of the UML using the pUML OO Meta Modeling Approach, available from: http://www.klasse.nl/english/uml/uml-semantics.html.
[Mot96] R. Motschnig-Pitrik. Analyzing the notions of attribute, aggregate, part and member in data/knowledge modeling. The Journal of Systems and Software, 33(2):113–122, May 1996.
[Pri97] S. Pribbenow. What’s a part? On formalizing part-whole relations. In Foundations of Computer Science: Potential – Theory – Cognition, volume 1337 of LNCS, pages 399–406. Springer, 1997.
[Richters1998] Mark Richters and Martin Gogolla. On formalizing the UML Object Constraint Language OCL. In Tok Wang Ling, Sudha Ram, and Mong Li Lee, editors, Proc. 17th Int. Conf. Conceptual Modeling (ER’98), volume 1507 of LNCS, pages 449–464. Springer, 1998.
[Richters1999] Mark Richters and Martin Gogolla, A metamodel for OCL, in Robert France and Bernhard Rumpe, editors, UML’99 - The Unified Modeling Language. Beyond the Standard. Second International Conference, Fort Collins, CO, USA, October 28-30. 1999, Proceedings, volume 1723 of LNCS. Springer, 1999.
[Ric02] M. Richters. A Precise Approach to Validating UML Models and OCL Constraints. Ph.D. thesis, Universit ̈at Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14, 2002.
[Tho99] S. Thompson. Haskell: The Craft of Functional Programming. Addison-Wesley, 2nd edition, 1999. [Warmer98] Jos Warmer en Anneke Kleppe, The Object Constraint Language: precise modeling with UML,
Addison-Wesley, 1999.
15
[15] 酒井政裕，今井健男:SAT 問題と他の制約問題と の相互発展, コンピュータソフトウェア, Vol. 32, No. 1 (2015), pp. 103–119.
16
[16] Satoh, K., Asai, K., Kogawa, T., Kubota, M.,
Nakamura, M., Nishigai, Y., Shirakawa, K., Takano, C.: “PROLEG: An Implementation of the Presup- posed Ultimate Fact Theory of Japanese Civil Code by PROLOG Technology”, New Frontiers in Arti- ficial Intelligence: JSAI-isAI 2010 Workshops, Re- vised Selected Papers, LNAI 6797, (2012), pp. 153– 164.
17
[17] Sergot, M.J., Sadri, F., Kowalski, R.A., Kri- waczek, F., Hammond, P., Cory, H. T., “The British Nationality Act as a Logic Program”, Communica- tions of the ACM, Vol. 29 No. 5 (1986), pp. 370–386.
17.1
- Allen, L.E. Symbolic logic: A razor-edged tool for drafting and inter- preting legal documents. Yale Law I, 66 (May 1957). 833-879.
- Bench-Cauon. T.. and Seraot. M.1. Towards a rule-based reoresenta- tion of opkn texture in La<. Rep.. Dept. of Computing, Imperial
College, London. 1965. Also presented at the 2nd International
Con-ference on Computers and Law, Houston. Tex.. June 1985.
3 Bobrow, D.G., Ed. Non-monotonic logic. Special issue on. Altif. Infell.13 (1980). - Bowen. K.A., and Kowalski. R.A. Amalgamating language and meta-
language in logic programming. In Logic Programming. K.L. Clark and S.A. Tarnlund. Eds. APIC Studies in Data Processing, vol. 16. Aca- demic Press. New York, 1982. pp. 153-172. - Bowen. K.A., and Weinberg, T. A meta-level extension of PROLOG. In Symposium on Logic Programming (Boston. Mass.). IEEE Computer Society Press, 1985, pp. 48-53.
- Ghan, D. A logic based legal expert. M.S. thesis. Dept. of Computing, Imperial College, London. 1984.
- Clark, K.L. Negation as failure. In Logic and Data Bases, H. Callaire and J. Minker, Eds. Plenum, New York, 1978. pp. 293-322.
- Clark, K.L., and McCabe. F.G. Micro-PROLOG: Programming in Logic. Prentice-Hall. Englewood Cliffs, N.J.. 1984.
- de Marco, T. Strucfured Analysis and System Specific&w?. Prentice- Hall, Englewood Cliffs, N.J.. 1979.
IO. Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J.. 1976. - Feigenbaum, E.A.. and McCorduck, P. The Fiffh Generation. Addison- Wesley, Reading. Mass., 1983.
- Fuchi. K. The direction the FGCS project will take. New Generation Comput. I (1983). 3-9.
- Gardner. A.V.D.L. An artificial intelligence approach to legal reason- ing. Rep. STAN-CS-85-1045. Dept. of Computing Science, Stanford Univ., 1984. To be published by Bradford Books/MIT Press.
- Gardner, A.V.D.L. Overview of an artificial intelligence approach to legal reasoning. In Computing Power nnd Legal Reasoning, C. Walter, Ed. West. St. Paul. Minn.. 1985. pp. 247-274.
- Genesereth. M.R., Greiner, R., Grinberg, M.R., and Smith. D.E. The MRS dictionary. Memo HPP-80.24, Stanford Heuristic Programming Project. Stanford IJniv., Calif., Dec. 1980: revised Jan. 1984.
- Gordon, T.F. Object-oriented predicate logic and its role in repre- senting legal knowledge. In Computing Power and Legal Reasoning, C. Walter. Ed. West, St. Paul. Minn.. 1985. pp. 163-203.
- Hammond. P. Representation of DHSS regulations as a logic pro- gram. Rep. 82/X, Dept. of Computing, Imperial College, London. 1982. pp. 225-235. Also in Proceedings offhe 3rd KS Expert Systems Conference, British Computer Society, Cambridge, Dec. 1983.
pp. 225-235. - Hammond. P., and Sergot. M.J. A PROLOG shell for logic based
expert systems. In Proceedings of the 3rd BCS Experf Systems Confer-
once. British Computer Society. Cambridge, Dec. 1983, pp. 95-104. - Hammond, J’., and Sergot, M.J. APES Rejerence Manual. Logic Based
Systems. Richmond, Surrey. England, 1984. - Her Majesty’s Stationery Office. The British Nationality Act 1981. Chapter 61, London, 1981.
- Hustler, A. ProgrammIng law in logic. Res. Rep. CS-82-13, Dept. of Computer Science, Univ. of Waterloo. Canada, 1982.
- Jones, S. Control structures in legislation. In Compufer Science and Law, 8. Niblett. Ed. Cambridge University Press, New York, 1980.
pp. 157-l 69. - Jones, S.. Mason, P., and Stamper. R. LEGOL 2.0: A relational specification language for co,mplex rules. Inf Sysf. 4, 4 (Dec. 1979). 293-305.
- Kowalski. R.A. Logic for Problem Solving. Elsevier North-Holland,
New York, 1979. - Kowalski, R.A. Logic programming. In Proceedings ZNP-83 Congress.
Elsevier North-Holland. New York, 1983. pp. 133-145. - Kowalski, R.A. Software engineering and knowledge-based systems
in new generation computing. Future Generation Compuf. Sysf. 1. 1 (1984), 39-49.
27.Lakatos, 1. Proofs and refutations. Br. J. Philos. Sci. 14 (1963). l-25, 120-139. 221-243. 296-342.
28.Lloyd. J.W., and Topor, R.W. Making Prolog more expressive. /. Logic Program. I. 3 (Oct. 1984). 225-240.
29.Lowes. D. Assistance to industry: A logical approach. MS. thesis. Dept. of Computing. Imperial College. London, 1984.
30 MacRae, C.D. User control knowledge in a tax consulting system. In 2nd Infernational Conference on Computers and Law (Houston. Tex.. June). 1985.
31 McCarthy. L.T. Reflections on TAXMAN: An experiment in artifi-
cial intelligence and legal reasoning. Harvard Law Rev. 90 (1977). 837-893.
32 McCarthy, L.T.. and Sridharan. N.S. The representation of an evolv- ing system of legal concepts: I. Logical templates. In Proceedings, 3rd Biennial Conference offhe Canadian Society forCompufafional Studies of lnfelligence (Victoria. B.C.). Canadian Society for Computational Studies of Intelligence, 1980. pp. 304-311.
33 Meldman. J.A. A siructural model for computer-aided legal analysis. Rufgers 1. Compuf. Law 6 (1977). 27-71. - Schlobohm, D.A. A Prolog program which analyzes income tax is- sues under Section 318(a) of the internal revenue code. In Computing Power and Legal Reasoning, C. Walter. Ed. West, St. Paul. Minn.,
- pp. 765-815.
- Sergot, M.J. Programming law: LEGOL as a logic programming lan- guage. Rep., Dept. of Computing, Imperial Collage, London, 1980.
- Sergot. M.J. Representing legislation as logic programs. Rep.. Dept. of Computing. Imperial College. Aug. 1985. To be published in
Machine Infelligence 17. - Sharpe, W.P. Logic programming for the law. In Research and Dew- opmenf in Experf Systems: Proceedings ofthe 4th Technical Conference of fhe British Compufer Society Specialisf Group on Experf Systems, War- wick, M.A. Braines, Ed. Cambridge University Press, New York, Dec. 1985.
- Stamper, R. LEGOL: Modelling legal rules by computer. In Computer Science and Law, B. Niblett. Ed. Cambridge University Press, New York, 1980, pp. 45-71.
- Suphamongkhon. K. Towards an expert system op immigration leg- islation. M.S. thesis, Dept. of Computing. Imperial College, London, 1984.
- Sussman. G.. Winograd. T.. and Charniak, E. Micro-Planner refer- ence manual (revised). A.I. Memo 203A, Artificial Intelligence Labo- ratory. M.I.T.. Cambridge. Mass.. 1971.
- Szolovits, P.. Hawkinson. L.B., and Martin, W.A. An overview of OWL, a language for knowledge representation. MlT/LCS/TM-86. Laboratory for Computer Science, M&T., Cambridge. Mass.. 1977.
- Waterman, D.A., and Peterson. M.A. Models of legal decisionmak- ing. Rep. R-2717-ICJ, Institute for Civil Justice, Rand Corporation. Santa Barbara, Calif.. 1981.
18
[18] 島津明:国民年金法の構造的書き換え-法令工学の 立場から-，JAIST Press (2009).
##19
[19] 島津明:法令工学の提案, 第 2 章法令文書の言語処 理，JAIST Press (2007), pp. 21–50.
##20
[20] 職 業 安 定 局 文 書:
労働者派遣法改正法案の条文の誤りについて
職業安定局 平成 26 年5月 26 日
http://www.mhlw.go.jp/file/05-Shingikai-10201000-Daijinkanbousoumuka-Soumuka/0000046988.pdf
##21
[21] 田中リベカ，峯島宏次，Pascual Martinez-Gomez， 宮尾祐介，戸次大介:日本語 CCG パーザに基づく意味 解析・推論システムの提案, 言語処理学会 第 22 回年次 大会 発表論文集, (2016), pp. 757–760.
22
[22] 東条敏，Wong, S., 新田克己，横田一正:状況論理 による法的推論の形式化，情報処理学会論文誌 36 巻 1 号，(2007), pp. 51–60.
23
[23]
タイトルがないためみつからない。たぶん。
2つ以上の年金を受ける権利ができたとき
https://www.nenkin.go.jp/service/jukyu/tetsuduki/kyotsu/jukyu/20150501.html
2 岩沼 宏治, 鍋島 英知
岩沼 宏治, 鍋島 英知:「SMT:個別理論を取り扱う SAT 技術(<特集>最近の SAT 技術の発 展)」，人工知能学会誌，Vol. 25，No.1，pp. 86-95，2010
[有川88) 有川節夫,，原口誠: 述語論理と論理プログラミング， オーム社 (198)
[Armando0]Armando,A.,Castelini,C.andGiunchiglia,E.: SAT-basedproceduresfortemporalreasoning,Proc.5th EuropeanConf.onPlaning,LNCS1809,p.97-108 (20)
[Bryand01]Bryand,R.,German,S.andVelev,M.:Processor verificationusingeficientreductionsofthelogicof uninterpretedfunctionstopropositionallogic,ACMTrans.on ComputationalLogic,Vol.2,No.1,p.93-134(201)
[Barrett02] Barrett,C.W.,Dil,D.L.andStump,A.:A generalizationofShostak'smethodforcombiningdecision procedures,Proc.4thInt.WS.onFrontiersofCombining Systems (FroCoS'2002),LNCS2309,p.132-147 (202)
[Baret09a]Baret,B.,Deters,M.,Oliveras,A andStump,A.: InternationalSatisfiabilityModuloTheoriesCompetition, http://www.smtcomp.org/
[Baret09b]Baret,C.,Sebastiani,R.,Seshia,S.A.andTineli, C.:Satisfiabilitymodulotheories,HandbookofSatisfiability, Chapter26,p.825-85,IOSPres (209)
[Downey78]Downey,P.andSethi,R.:Assignmentcommands witharrayreferences,J.ACM,Vol.25,No.4,p.652-666
(1978) [Downey80]Downey,P.,Sethi,R.andTarjan,R.E.:Variationson the common subexpres sion problem,J.ACM,Vol.27,No.4,p p. 757-71 (1980) [Flangan03]Flangan,J.,Joshi,R.,Ou,X.andSaxe,J.B.:
Theoremprovingusinglazyprofexplanation,Proc.15thInt.
Conf.onComputerAidedVerification (CAV),LNCS2725 (20 03) [Ganzinger02]Ganzinger,H.:Shostaklight,Proc.18thInt.Conf. onAutomatedDeduction (CADE-18),LNAI2392,p p.332-346
(202)
[萩谷 94]萩谷昌己:ソフトウェア科学のための論理学，岩沼書店(194)
[井上 08]井上克已坂間千秋:論理プログラミングから解集合 プ ロ グ ラ ミ ン グ へ コンピュータソフトウェア， Vol.25,No.3, p.20-32 (208)
[岩沼 09]岩沼宏治，鍋島英知，井上克巳:一階論理上の等号推論 理論と実際，コンピュータソフトウェア(投稿予定)
[ J a f f e r 9 4 ] J a f f a r , J . a n d M a h e r , M . : C o n s t r a i n t l o g i c p r o g r a m m i n g : A S u r v e Y , J. L o g i c P r o g r a m m i n g , V o l . 1 9 / 2 0 , p p . 503-581 (194)
[Karmakar84]Karmakar,N.:A newpolynomial-timealgorithm forlinearprogramming,Combinatorica,Vol.4,No.4,p. 373-395 (1984)
[Letz94]Letz,R.,Goler,C.andMayr,K.:Controledintegration ofthecutruleintoconectiontableaucalculi,J.Automated Reasoning,Vol.13,p.297-338 (194)
[Lahiri04]Lahiri,S.K.andSeshia,S.A.:TheUCLIDDecision procedure,Proc.16thInt.Conf.onComputerAidedVerification
(CAV),LNCS314,p.475-478 (204) [Manna03]Manna,Z.andZarba,C.G.:Combiningdecision procedures,FormalMethodsattheCrosroads:FromPanacea toFoundationalSuport,LNCS2757,p.381-422
(203) [鍋島 10]鍋島英知，宋剛秀:高速 SATソルバーの原理`人工知
能 学 会 誌 Vol.25,No.1,p.68-76 (2010)
[Navarro-Perez07]Navarro-Perez,J.A.andVoronkov,A.:
EncodingsofboundedLTLmodelcheckinginefectively propositionallogic,Proc.21stInt.ConfonAutomated Deduction (CADE-21),LNAI4603,p.346部 1 (207)
[Nelson79]Nelson,G.andOppen,D.C.:Simplificationby coperatingdecisionprocedures,ACMTrans.onProgramming LanguagesandSystems,Vol.1,No.2,p.245-257 (1979)
[Nelson80]Nelson,G.andOppen,D.C.:Fastdecisionprocedures basedoncongruenceclosure,J.ACM,Vol.27,No.2,p. 356-364 (1980)
[Nelson84]Nelson,G.:Combiningsatisfiabilityproceduresby equalitysharing,AutomatedTheoremProving:After25Years, Vol.29ofContemporaryMathematics,p.201-21,American MathematicalSociety (1984)
[Nieuwenhuis05}Nieuwenhuis,R.andOliveras,A.:Prof-
producingcongruenceclosure,Proc.16thInt.ConfonTerm RewritingandApplications (RTA'05),LNCS3467,p. 453-468 (205)
[Nieuwenhuis05b]Nieuwenhuis,R.andOliveras,A.:DPLL (T) withexhaustivetheorypropagationanditsaplication todiferencelogic,Proc.17thInt.ConfonComputerAided
Verification (CAV'05),LNCS3576,p.321-334 (205) [Nieuwenhuis06]Nieuwenhuis,R.,Oliveras,A andTineli, C.:SolvingSATandSATmodulotheories:Fromanabstract
Davis-Putnam-Logemann-LovelandproceduretoDPLL (T)
J.ACM,Vol.53,No.6,p.937-977 (206) [Nieuwenhuis01]Nieuwenhuis,R.andRubio,A.:Para-
modulation-BasedTheoremProving,HandbookofAutomated Reasoning,Vol.1,Chapter7,p.373-43,ElsevierScience B.V. (201)
[Oppen80a]Oppen,D.C.:Complexity,convexityandcombi- nationsoftheories,TheoreticalComputerScience,Vol.12,p. 291-302 (1980)
[Oppen80b]Oppen,D.C.:Reasoningaboutrecursivelydefined datastructures,J.ACM,Vol.27,No.3,p p.403-411 (1980)
[Papadimitriou81]Papadimitriou,C.H.:Onthecomplexity ofintegerprogramming,J.ACM,Vol.28,No.4,p.765-768
(1981)
[Ranise 06] Ranise, S. and Tinel li, C.: Satisfiability modulo
theories:Trendsandcontroversies,IEEEInteligenceSystems
Magazine,Vol.21,No.6,p p.71-81 (20 06) [Shankar02]Shankar,N.andRues,H.:CombiningShostak
theories,Proc.ofInter.ConfonRewritingTechniquesand
Aplications (RTA),LNCS,Vol.2378,p.1-18 (202) [Stump01]Stump,A.,Baret,C.W,Dil,D.L.andLevit,J.:A decisionprocedureforanextensionaltheoryofarays,Proc.
17thIEEESymp.onLogicinComputerScience,p.29-37 (201)
[Suzuki80]Suzuki,N.andJaferson,D.:Verificationdecidability o f P r e s b u r g e r a r r a y p r o g r a m s , J. A C M , V o l . 2 7 , N o . 1, p p . 1 9 1 - 2 0 5 ( 1 9 8 0 )
[Shostak84]Shostak,R.E.:Decidingcombinationoftheories,J. ACM,Vol.31,No.1,p.1-12 (1984)
[田村 10]田村直之，丹生智也，番原陸則:制約最適化問題と SAT 符号化，人工知能学会誌， Vol.25,No.1,p.7-85 (2010)
[Tineli04]Tineli,C.:Thecombinationprobleminfirst-orderlogic theunsortedcase,Proc.CombinationofDecisionProcedures: SummerSchool204,http://verify.stanford.edu/ summerschool2004/
[Tineli05]Tineli,C.andZarba,C.G.:Combiningnonstably infinitetheories,J.AutomatedReasoning,Vol.34,No.3,p. 209-238 (205)
その他
法令工学の実践
国民年金法の述語論理による記述と検証
片山 卓也
katayama@jaist.ac.jp
第3版 (2020 年 11 月) JAIST Press
https://dspace.jaist.ac.jp/dspace/bitstream/10119/16096/1/fulltext.pdf
<この項は書きかけです。順次追記します。>
This article is not completed. I will add some words and/or centences in order.
Este artículo no está completo. Agregaré algunas palabras en orden.
知人資料
' @kazuo_reve 私が効果を確認した「小川メソッド」
https://qiita.com/kazuo_reve/items/a3ea1d9171deeccc04da
' @kazuo_reve 新人の方によく展開している有益な情報
https://qiita.com/kazuo_reve/items/d1a3f0ee48e24bba38f1
' @kazuo_reve Vモデルについて勘違いしていたと思ったこと
https://qiita.com/kazuo_reve/items/46fddb094563bd9b2e1e
自己記事一覧
Qiitaで逆リンクを表示しなくなったような気がする。時々、スマフォで表示するとあらわることがあり、完全に削除したのではなさそう。2024年４月以降、せっせとリンクリストを作り、統計を取って確率を説明しようとしている。2025年２月末を目標にしていた。
一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39
views 20,000越え自己記事一覧
https://qiita.com/kaizen_nagoya/items/58e8bd6450957cdecd81
Views１万越え、もうすぐ１万記事一覧 最近いいねをいただいた216記事
https://qiita.com/kaizen_nagoya/items/d2b805717a92459ce853
仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df
Qiita(0)Qiita関連記事一覧（自分）
https://qiita.com/kaizen_nagoya/items/58db5fbf036b28e9dfa6
Error一覧 error(0)
https://qiita.com/kaizen_nagoya/items/48b6cbc8d68eae2c42b8
C++ Support(0)
https://qiita.com/kaizen_nagoya/items/8720d26f762369a80514
Coding(0) Rules, C, Secure, MISRA and so on
https://qiita.com/kaizen_nagoya/items/400725644a8a0e90fbb0
Ethernet 記事一覧 Ethernet(0)
https://qiita.com/kaizen_nagoya/items/88d35e99f74aefc98794
Wireshark 一覧 wireshark(0)、Ethernet(48)
https://qiita.com/kaizen_nagoya/items/fbed841f61875c4731d0
線網（Wi-Fi）空中線(antenna)(0) 記事一覧(118/300目標)
https://qiita.com/kaizen_nagoya/items/5e5464ac2b24bd4cd001
なぜdockerで機械学習するか 書籍・ソース一覧作成中 (目標100)
https://qiita.com/kaizen_nagoya/items/ddd12477544bf5ba85e2
プログラムちょい替え（0）一覧:4件
https://qiita.com/kaizen_nagoya/items/296d87ef4bfd516bc394
言語処理100本ノックをdockerで。python覚えるのに最適。:10+12
https://qiita.com/kaizen_nagoya/items/7e7eb7c543e0c18438c4
Python(0)記事をまとめたい。
https://qiita.com/kaizen_nagoya/items/088c57d70ab6904ebb53
安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409
プログラマによる、プログラマのための、統計(0)と確率のプログラミングとその後
https://qiita.com/kaizen_nagoya/items/6e9897eb641268766909
転職(0)一覧
https://qiita.com/kaizen_nagoya/items/f77520d378d33451d6fe
技術士(0)一覧
https://qiita.com/kaizen_nagoya/items/ce4ccf4eb9c5600b89ea
Reserchmap(0) 一覧
https://qiita.com/kaizen_nagoya/items/506c79e562f406c4257e
物理記事 上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff
量子(0) 計算機, 量子力学
https://qiita.com/kaizen_nagoya/items/1cd954cb0eed92879fd4
数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d
coq(0) 一覧
https://qiita.com/kaizen_nagoya/items/d22f9995cf2173bc3b13
統計(0)一覧
https://qiita.com/kaizen_nagoya/items/80d3b221807e53e88aba
図(0) state, sequence and timing. UML and お絵描き
https://qiita.com/kaizen_nagoya/items/60440a882146aeee9e8f
色(0) 記事100書く切り口
https://qiita.com/kaizen_nagoya/items/22331c0335ed34326b9b
品質一覧
https://qiita.com/kaizen_nagoya/items/2b99b8e9db6d94b2e971
言語・文学記事 １００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6
医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82
水の資料集(0) 方針と成果
https://qiita.com/kaizen_nagoya/items/f5dbb30087ea732b52aa
自動車 記事 １００
https://qiita.com/kaizen_nagoya/items/f7f0b9ab36569ad409c5
通信記事１００
https://qiita.com/kaizen_nagoya/items/1d67de5e1cd207b05ef7
日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68
英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d
音楽 一覧(0)
https://qiita.com/kaizen_nagoya/items/b6e5f42bbfe3bbe40f5d
「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b
鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/faa4ea03d91d901a618a
OSEK OS設計の基礎 OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3
coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68
官公庁・学校・公的団体（NPOを含む）システムの課題、官（０）
https://qiita.com/kaizen_nagoya/items/04ee6eaf7ec13d3af4c3
「はじめての」シリーズ ベクタージャパン
https://qiita.com/kaizen_nagoya/items/2e41634f6e21a3cf74eb
AUTOSAR(0)Qiita記事一覧, OSEK(75)
https://qiita.com/kaizen_nagoya/items/89c07961b59a8754c869
プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945
LaTeX(0) 一覧
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792
自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b
Rust(0) 一覧
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927
programの本質は計画だ。programは設計だ。
https://qiita.com/kaizen_nagoya/items/c8545a769c246a458c27
登壇直後版 色使い(JIS安全色) Qiita Engineer Festa 2023〜私しか得しないニッチな技術でLT〜 スライド編 0.15
https://qiita.com/kaizen_nagoya/items/f0d3070d839f4f735b2b
プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945
逆も真：社会人が最初に確かめるとよいこと。OSEK(69)、Ethernet(59)
https://qiita.com/kaizen_nagoya/items/39afe4a728a31b903ddc
統計の嘘。仮説（127）
https://qiita.com/kaizen_nagoya/items/63b48ecf258a3471c51b
自分の言葉だけで論理展開できるのが天才なら、文章の引用だけで論理展開できるのが秀才だ。仮説（136）
https://qiita.com/kaizen_nagoya/items/97cf07b9e24f860624dd
参考文献駆動執筆(references driven writing)・デンソークリエイト編
https://qiita.com/kaizen_nagoya/items/b27b3f58b8bf265a5cd1
「何を」よりも「誰を」。１０年後のために今見習いたい人たち
https://qiita.com/kaizen_nagoya/items/8045978b16eb49d572b2
Qiitaの記事に３段階または５段階で到達するための方法
https://qiita.com/kaizen_nagoya/items/6e9298296852325adc5e
出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840
祝休日・謹賀新年 2025年の目標
https://qiita.com/kaizen_nagoya/items/dfa34827932f99c59bbc
Qiita 1年間をまとめた「振り返りページ」＠2024
https://qiita.com/kaizen_nagoya/items/ed6be239119c99b15828
2024 参加・主催Calendarと投稿記事一覧 Qiita(248)
https://qiita.com/kaizen_nagoya/items/d80b8fbac2496df7827f
主催Calendar2024分析 Qiita(254)
https://qiita.com/kaizen_nagoya/items/15807336d583076f70bc
Calendar 統計
https://qiita.com/kaizen_nagoya/items/e315558dcea8ee3fe43e
LLM 関連 Calendar 2024
https://qiita.com/kaizen_nagoya/items/c36033cf66862d5496fa
Large Language Model Related Calendar
https://qiita.com/kaizen_nagoya/items/3beb0bc3fb71e3ae6d66
博士論文 Calendar 2024 を開催します。
https://qiita.com/kaizen_nagoya/items/51601357efbcaf1057d0
博士論文(0)関連記事一覧
https://qiita.com/kaizen_nagoya/items/8f223a760e607b705e78
coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68
あなたは「勘違いまとめ」から、勘違いだと言っていることが勘違いだといくつ見つけられますか。人間の間違い(human error(125))の種類と対策
https://qiita.com/kaizen_nagoya/items/ae391b77fffb098b8fb4
プログラマの「プログラムが書ける」思い込みは強みだ。３つの理由。仮説（168）統計と確率(17) , OSEK(79)
https://qiita.com/kaizen_nagoya/items/bc5dd86e414de402ec29
出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840
これからの情報伝達手段の在り方について考えてみよう。炎上と便乗。
https://qiita.com/kaizen_nagoya/items/71a09077ac195214f0db
ISO/IEC JTC1 SC7 Software and System Engineering
https://qiita.com/kaizen_nagoya/items/48b43f0f6976a078d907
アクセシビリティの知見を発信しよう！（再び）
https://qiita.com/kaizen_nagoya/items/03457eb9ee74105ee618
統計論及確率論輪講（再び）
https://qiita.com/kaizen_nagoya/items/590874ccfca988e85ea3
読者の心をグッと惹き寄せる7つの魔法
https://qiita.com/kaizen_nagoya/items/b1b5e89bd5c0a211d862
「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b
ソースコードで議論しよう。日本語で議論するの止めましょう（あるプログラミング技術の議論報告）
https://qiita.com/kaizen_nagoya/items/8b9811c80f3338c6c0b0
脳内コンパイラの3つの危険
https://qiita.com/kaizen_nagoya/items/7025cf2d7bd9f276e382
心理学の本を読むよりはコンパイラ書いた方がよくね。仮説（34）
https://qiita.com/kaizen_nagoya/items/fa715732cc148e48880e
NASAを超えるつもりがあれば読んでください。
https://qiita.com/kaizen_nagoya/items/e81669f9cb53109157f6
データサイエンティストの気づき!「勉強して仕事に役立てない人。大嫌い!!」『それ自分かも?』ってなった!!!
https://qiita.com/kaizen_nagoya/items/d85830d58d8dd7f71d07
「ぼくの好きな先生」「人がやらないことをやれ」プログラマになるまで。仮説（37）
https://qiita.com/kaizen_nagoya/items/53e4bded9fe5f724b3c4
なぜ経済学徒を辞め、計算機屋になったか（経済学部入学前・入学後・卒業後対応） 転職(1)
https://qiita.com/kaizen_nagoya/items/06335a1d24c099733f64
プログラミング言語教育のXYZ。 仮説（52）
https://qiita.com/kaizen_nagoya/items/1950c5810fb5c0b07be4
【24卒向け】9ヶ月後に年収１０００万円を目指す。二つの関門と三つの道。
https://qiita.com/kaizen_nagoya/items/fb5bff147193f726ad25
「【25卒向け】Qiita Career Meetup for STUDENT」予習の勧め
https://qiita.com/kaizen_nagoya/items/00eadb8a6e738cb6336f
大学入試不合格でも筆記試験のない大学に入って卒業できる。卒業しなくても博士になれる。
https://qiita.com/kaizen_nagoya/items/74adec99f396d64b5fd5
全世界の不登校の子供たち「博士論文」を書こう。世界子供博士論文遠隔実践中心 安全(99)
https://qiita.com/kaizen_nagoya/items/912d69032c012bcc84f2
日本のプログラマが世界で戦える16分野。仮説(53),統計と確率(25) 転職(32)、Ethernet(58)
https://qiita.com/kaizen_nagoya/items/a7e634a996cdd02bc53b
小川メソッド 覚え（書きかけ）
https://qiita.com/kaizen_nagoya/items/3593d72eca551742df68
DoCAP（ドゥーキャップ）って何ですか？
https://qiita.com/kaizen_nagoya/items/47e0e6509ab792c43327
views 20,000越え自己記事一覧
https://qiita.com/kaizen_nagoya/items/58e8bd6450957cdecd81
Views１万越え、もうすぐ１万記事一覧 最近いいねをいただいた213記事
https://qiita.com/kaizen_nagoya/items/d2b805717a92459ce853
amazon 殿堂入りNo1レビュアになるまで。仮説(102)
https://qiita.com/kaizen_nagoya/items/83259d18921ce75a91f4
100以上いいねをいただいた記事16選
https://qiita.com/kaizen_nagoya/items/f8d958d9084ffbd15d2a
水道局10年(1976,4-1986,3)を振り返る
https://qiita.com/kaizen_nagoya/items/707fcf6fae230dd349bf
小川清最終講義、最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on my individual experience. It has nothing to do with the organization or business to which I currently belong.
Este artículo es una impresión personal basada en mi experiencia personal. No tiene nada que ver con la organización o empresa a la que pertenezco actualmente.
文書履歴(document history)
ver. 0.01 初稿 20190525
ver. 0.02 URL, 参考文献 20211005
ver. 0.03 参考文献の参考文献 20211007
ver. 0.04 URL追記 20230210
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.
Muchas gracias por leer hasta la última oración.
Por favor, haz clic en el ícono Me gusta 💚 y sígueme para tener una vida feliz.