Z3
https://github.com/z3prover/z3
Z3Py チュートリアル
$ 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
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
thecommonsubexpres sionproblem,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-
95
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)
2和
[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
文書履歴
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.