Skip to main content
SpringerLink
Log in

On First-Order Model-Based Reasoning

  • Chapter
  • First Online:
Logic, Rewriting, and Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9200))

Abstract

Reasoning semantically in first-order logic is notoriously a challenge. This paper surveys a selection of semantically-guided or model-based methods that aim at meeting aspects of this challenge. For first-order logic we touch upon resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we give a preview of a new method called SGGS, for Semantically-Guided Goal-Sensitive reasoning. For first-order theories we highlight hierarchical and locality-based methods, concluding with the recent Model-Constructing satisfiability calculus.

Dedicated to

José Meseguer,

friend and colleague.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Other approaches to subdivide work between superposition and an SMT-solver appeared in [20, 25].

  2. 2.

    The problem in Examples 10 and 11 appeared in the slides of a talk entitled “Arithmetic and Optimization @ MCsat” presenting joint work by Leonardo de Moura, Dejan Jovanović, and Grant Olney Passmore, and given by Leonardo de Moura at a Schloss Dagsthul Seminar on “Deduction and Arithmetic” in October 2013.

References

  1. Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84–99. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Aravindan, C., Baumgartner, P.: Theorem proving techniques for view deletion in databases. J. Symbolic Comput. 29(2), 119–148 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  3. Arthan, R., Oliva, P.: (Dual) Hoops have unique halving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 165–180. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM 45(6), 1007–1049 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  7. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 26, pp. 825–886. IOS Press, Amsterdam (2009)

    Google Scholar 

  8. Baumgartner, P., Fröhlich, P., Furbach, U., Nejdl, W.: Semantically guided theorem proving for diagnosis applications. In: Proceedings of IJCAI-16, vol. 1, pp. 460–465 (1997)

    Google Scholar 

  9. Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006)

    Article  MATH  Google Scholar 

  10. Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: Alferes, J.J., Moniz Pereira, L., Orłowska, E. (eds.) JELIA 1996. LNCS (LNAI), vol. 1126, pp. 1–17. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  11. Baumgartner, P., Furbach, U., Pelzer, B.: The hyper tableaux calculus with equality and an application to finite model computation. J. Logic Comput. 20(1), 77–109 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  12. Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution calculus with equality - revised and implemented. J. Symbolic Comput. 47(9), 1011–1045 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  13. Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  14. Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 17–34. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 39–57. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Bender, M., Pelzer, B., Schon, C.: System description: E-KRHyper 1.4 – Extensions for unique names and description logic. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 126–134. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Bibel, W., Schmitt, P.H. (eds.): Automated Deduction - A Basis for Applications (in 2 volumes). Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  18. Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Veloso, M.M., Wooldridge, M.J. (eds.) Artificial Intelligence Today - Recent Trends and Developments. LNCS (LNAI), vol. 1600, pp. 43–84. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fernández, M. (eds.): Proceedings of PPDP-12, pp. 1–11. ACM Press (2010)

    Google Scholar 

  20. Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symbolic Comput. 45(2), 229–260 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  21. Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoret. Comput. Sci. 146, 199–242 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  22. Bonacina, M.P., Hsiang, J.: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. New Gener. Comput. 16(2), 163–200 (1998)

    Article  MathSciNet  Google Scholar 

  23. Bonacina, M.P., Johansson, M.: Interpolation of ground proofs in automated deduction: a survey. J. Autom. Reasoning 54(4), 353–390 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  24. Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reasoning 54(1), 69–97 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  25. Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161–189 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  26. Bonacina, M.P., Plaisted, D.A.: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of UNIF-28, RISC Technical Reports, pp. 47–54. Johannes Kepler Universität, Linz (2014)

    Google Scholar 

  27. Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) Proceedings of PAAR-4, EasyChair Proceedings in Computing (EPiC), pp. 25–38 (2015)

    Google Scholar 

  28. Bonacina, M.P., Plaisted, D.A.: Semantically guided goal-sensitive reasoning: inference system and completeness (2015, in preparation)

    Google Scholar 

  29. Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reasoning 55(1), 1–29 (2015). doi:10.1007/s10817-015-9334-4

    Article  MathSciNet  MATH  Google Scholar 

  30. Boy de la Tour, T., Echenim, M.: Permutative rewriting and unification. Inf. Comput. 205(4), 624–650 (2007)

    Google Scholar 

  31. Chang, C.-L., Lee, R.C.-T.: Symbolic logic and mechanical theorem proving. Academic Press, New York (1973)

    MATH  Google Scholar 

  32. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  33. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  34. de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  35. de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  36. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier, Amsterdam (1990)

    Google Scholar 

  37. Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theoret. Comput. Sci. 238, 103–119 (2009)

    Article  MATH  Google Scholar 

  38. Fitelson, B.: Gibbard’s collapse theorem for the indicative conditional: an axiomatic approach. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 181–188. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  39. Furbach, U., Schon, C.: Semantically guided evolution of \({\cal S}{\cal H}{\cal I}\) ABoxes. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 17–34. Springer, Heidelbeg (2013)

    Chapter  Google Scholar 

  40. Gallier, J.H., Snyder, W.: Designing unification procedures using transformations: a survey. EATCS Bull. 40, 273–326 (1990)

    MATH  Google Scholar 

  41. Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 240(10), 1453–1492 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  42. Ganzinger, H., Waldmann, U.: Theorem proving in cancellative abelian monoids. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE-13. LNCS, vol. 1104, pp. 388–402. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  43. Goguen, J., Meseguer, J.: Order-sorted unification. J. Symbolic Comput. 8(4), 383–413 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  44. Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105(2), 217–273 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  45. Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  46. Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electron. Notes Theoret. Comput. Sci. 290(3), 37–50 (2012)

    Article  MATH  Google Scholar 

  47. Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  48. Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559–587 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  49. Hsiang, J., Rusinowitch, M., Sakai, K.: Complete inference rules for the cancellation laws. In: Proceedings of IJCAI-10, pp. 990–992 (1987)

    Google Scholar 

  50. Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  51. Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 30–45. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  52. Marques-Silva, J.P., Sakallah, K.A.: GRASP: a new search algorithm for satisfiability. In: Proceedings of ICCAD 1996, pp. 220–227 (1997)

    Google Scholar 

  53. Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321. MIT Press, Cambridge (1991)

    Google Scholar 

  54. Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  55. Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of FMCAD-13. ACM and IEEE (2013)

    Google Scholar 

  56. Kapur, D.: An automated tool for analyzing completeness of equational specifications. In: Proceedings of ISSTA-94, pp. 28–43. ACM (1994)

    Google Scholar 

  57. Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  58. Lee, S.-J., Plaisted, D.A.: Eliminating duplication with the hyperlinking strategy. J. Autom. Reasoning 9, 25–42 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  59. Lifschitz, V., Morgenstern, L., Plaisted, D.A.: Knowledge representation and classical logic. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 1, pp. 3–88. Elsevier, Amsterdam (2008)

    Chapter  Google Scholar 

  60. Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)

    Article  Google Scholar 

  61. McCune, W.W.: OTTER 3.3 reference manual. Technical Report ANL/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne (2003)

    Google Scholar 

  62. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of DAC-39, pp. 530–535 (2001)

    Google Scholar 

  63. Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201–211. American Mathematical Society, Providence (1983)

    Google Scholar 

  64. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  65. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  66. Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233–264 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  67. Plaisted, D.A.: Mechanical theorem proving. In: Banerji, R.B. (ed.) Formal Techniques in Artificial Intelligence, pp. 269–320. Elsevier, Amsterdam (1990)

    Google Scholar 

  68. Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Vol. I: Logical Foundations, pp. 273–364. Oxford University Press, Oxford (1993)

    Google Scholar 

  69. Plaisted, D.A.: Automated theorem proving. Wiley Interdisciplinary Reviews: Cognitive Science 5(2), 115–128 (2014)

    MathSciNet  Google Scholar 

  70. Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedrich Vieweg & Sohns, Braunschweig (1997)

    Book  MATH  Google Scholar 

  71. Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reasoning 25, 167–217 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  72. Plotkin, G.: Building in equational theories. Mach. Intell. 7, 73–90 (1972)

    MathSciNet  MATH  Google Scholar 

  73. Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first order theories with equality. Mach. Intell. 4, 135–150 (1969)

    MathSciNet  MATH  Google Scholar 

  74. Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965)

    MathSciNet  MATH  Google Scholar 

  75. Robinson, J.A.: A machine oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  76. Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press, Amsterdam (2001)

    MATH  Google Scholar 

  77. Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symbolic Comput. 11(1 & 2), 21–50 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  78. Shearer, R., Motik, B., Horrocks, I.: HermiT: a highly efficient OWL reasoner. In: Ruttenberg, A., Sattler, U., Dolbear, C. (eds.) Proceedings of OWLED-5, vol. 432 of CEUR (2008)

    Google Scholar 

  79. Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. J. ACM 14(4), 687–697 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  80. Slaney, J., Lusk, E., McCune, W.: SCOTT: semantically constrained Otter system description. In: Bundy, A. (ed.) CADE-12. LNCS (LNAI), vol. 814, pp. 764–768. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  81. Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE-20. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  82. Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: the case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 47–71. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  83. Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4), 1–31, Paper 1 (2008)

    Google Scholar 

  84. Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoret. Comput. Sci. 208(1–2), 149–177 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  85. Waldmann, U.: Superposition for divisible torsion-free abelian groups. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS (LNAI), vol. 1421, pp. 144–159. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  86. Wos, L., Carson, D., Robinson, G.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536–541 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  87. Zhang, H., Zhang, J.: MACE4 and SEM: a comparison of finite model generators. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 101–130. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  88. Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol. 2392, pp. 295–313. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Acknowledgments

The first author thanks David Plaisted, for starting the research on SGGS and inviting her to join in August 2008; and Leonardo de Moura, for the discussions on MCsat at Microsoft Research in Redmond in June 2013. The third author’s work was partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, www.avacs.org).

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università Degli Studi di Verona, Verona, Italy

    Maria Paola Bonacina

  2. Fachbereich Informatik, Universität Koblenz-Landau, Koblenz, Germany

    Ulrich Furbach & Viorica Sofronie-Stokkermans

Authors
  1. Maria Paola Bonacina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ulrich Furbach
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Viorica Sofronie-Stokkermans
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maria Paola Bonacina .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V. (2015). On First-Order Model-Based Reasoning. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23165-5_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23164-8

  • Online ISBN: 978-3-319-23165-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation