Skip to main content
SpringerLink
Log in

E-unification for subsystems of S4

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1379))

Included in the following conference series:

Abstract

This paper is concerned with the unification problem in the path logics associated by the optimised functional translation method with the propositional modal logics K, KD, KT, KD4, S4 and S5. It presents improved unification algorithms for certain forms of the right identity and associativity laws. The algorithms employ mutation rules, which have the advantage that terms are worked off from the outside inward, making paramodulating into terms superfluous.

I thank H. Ganzinger, A. Herzig, U. Hustadt, A. Nonnengart, H. J. Ohlbach and especially the anonymous referees for their comments. This research was conducted while I was employed at the Max-Planck-Institut für Informatik in Saarbrücken, Germany, and was funded by the MPG and the DFG through the TraLos-Project.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Arnborg, S. and Tidén, E. (1985), Unification problems with one-sided distributivity, in J.-P. Jouannaud (ed.), Proc. Intern. Conf. on Rewriting Techniques and Applications, Vol. 202 of LNCS, Springer, pp. 398–406.

    Google Scholar 

  • Auffray, Y. and Enjalbert, P. (1992), Modal theorem proving: An equational viewpoint, Journal of Logic and Computation 2(3), 247–297.

    Article  MathSciNet  MATH  Google Scholar 

  • Comon, H., Haberstrau, M. and Jouannaud, J.-P. (1994), Syntacticness, cyclesyntacticness and shallow theories, Information and Computation 111(1), 154–191.

    Article  MathSciNet  MATH  Google Scholar 

  • Doggaz, N. and Kirchner, C. (1991), Completion for unification, Theoretical Computer Science 85, 231–251.

    Article  MathSciNet  MATH  Google Scholar 

  • Farinas del Cerro, L. and Herzig, A. (1989), Automated quantified modal logic, in P. B. Brazdil and K. Konolige (eds), Machine Learning, Meta-Reasoning and Logics, Kluwer, pp. 301–317.

    Google Scholar 

  • Farinas del Cerro, L. and Herzig, A. (1995), Modal deduction with applications in epistemic and temporal logics, in D. M. Gabbay, C. J. Hogger and J. A. Robinson (eds), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, Clarendon Press, Oxford, pp. 499–594.

    Google Scholar 

  • Herzig, A. (1989), Raisonnement automatique en logique modale et algorithmes d'unification., PhD thesis, Univ. Paul-Sabatier, Toulouse.

    Google Scholar 

  • Jaffar, J. (1990), Minimal and complete word unification, J. ACM 37(1), 47–85.

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  • Kirchner, C. and Klay, F. (1990), Syntactic theories and unification, in J. C. Mitchell (ed.), Proc. LICS'90, IEEE Computer Society Press, Philadelphia, pp. 270–277.

    Google Scholar 

  • Makanin, G. S. (1977), The problem of solvability of equations in a free semigroup, Math. USSR Sbornik 32(2), 129–198.

    Article  MATH  Google Scholar 

  • Ohlbach, H. J. (1988), A Resolution Calculus for Modal Logics, PhD thesis, Univ. Kaiserslautern, Germany.

    Google Scholar 

  • Ohlbach, H. J. (1991), Semantics based translation methods for modal logics, Journal of Logic and Computation 1(5), 691–746.

    Article  MathSciNet  MATH  Google Scholar 

  • Ohlbach, H. J. and Schmidt, R. A. (1997), Functional translation and second-order frame properties of modal logics, Journal of Logic and Computation 7(5), 581–603.

    Article  MathSciNet  MATH  Google Scholar 

  • Plotkin, G. (1972), Building-in equational theories, in B. Meltzer and D. Michie (eds), Machine Intelligence 7, American Elsevier, New York, pp. 73–90.

    Google Scholar 

  • Schmidt, R. A. (1998), E-unification for subsystems of S4, Research Report MPI-I-98-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany.

    Google Scholar 

  • Schulz, K. U. (1992), Makanin's algorithm for word equations: Two improvements and a generalization, in K. U. Schulz (ed.), Word Equations and Related Topics, Vol. 572 of LNCS, Springer, pp. 85–150.

    Google Scholar 

  • Zamov, N. K. (1989), Modal resolutions, Soviet Mathematics 33(9), 22–29. Translated from Izv. Vyssh. Uchebn. Zaved. Mat. 9 (328) (1989) 22–29.

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Manchester Metropolitan University, Chester Street, Ml 5GD, Manchester, UK

    Renate A. Schmidt

Authors
  1. Renate A. Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag

About this paper

Cite this paper

Schmidt, R.A. (1998). E-unification for subsystems of S4. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052364

Download citation

  • DOI: https://doi.org/10.1007/BFb0052364

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64301-2

  • Online ISBN: 978-3-540-69721-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation