[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A Resolution Decision Procedure for Fluted Logic

  • Conference paper
Automated Deduction - CADE-17 (CADE 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1831))

Included in the following conference series:

Abstract

Fluted logic is a fragment of first-order logic without function symbols in which the arguments of atomic subformulae form ordered sequences. A consequence of this restriction is that, whereas first-order logic is only semi-decidable, fluted logic is decidable. In this paper we present a sound, complete and terminating inference procedure for fluted logic. Our characterisation of fluted logic is in terms of a new class of so-called fluted clauses. We show that this class is decidable by an ordering refinement of first-order resolution and a new form of dynamic renaming, called separation.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Article  MATH  MathSciNet  Google Scholar 

  2. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)

    Google Scholar 

  3. Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 83–96. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  4. de Nivelle, H.: A resolution decision procedure for the guarded fragment. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 191–204. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  5. Fermüller, C., Leitsch, A., Tammet, T., Zamov, N.: Resolution Methods for the Decision Problem. LNCS, vol. 679. Springer, Heidelberg (1993)

    MATH  Google Scholar 

  6. Fermüller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)

    Google Scholar 

  7. Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Fourteenth Annual IEEE Symposium on Logic in Computer Science, pp. 295–303. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  8. Gargov, G., Passy, S.: A note on Boolean modal logic. In: Petkov, P.P. (ed.) Mathematical Logic: Proceedings of the 1988 Heyting Summerschool, pp. 299–309. Plenum Press, New York (1990)

    Google Scholar 

  9. Goranko, V., Passy, S.: Using the universal modality: Gains and questions. J. Logic Computat. 2(1), 5–30 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  10. Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence 54, 319–379 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  11. Herzig, A.: A new decidable fragment of first order logic. In: Abstracts of the Third Logical Biennial, Summer School & Conference in Honour of S. C. Kleene, Varna, Bulgaria (1990)

    Google Scholar 

  12. Humberstone, I.L.: Inaccessible worlds. Notre Dame J. Formal Logic 24(3), 346–352 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  13. Humberstone, I.L.: The modal logic of ‘all and only’. Notre Dame J. Formal Logic 28(2), 177–188 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  14. Hustadt, U., Schmidt, R.A.: An empirical analysis of modal theorem provers. J. Appl. Non-Classical Logics 9(4) (1999)

    Google Scholar 

  15. Hustadt, U., Schmidt, R.A.: Maslov’s class K revisited. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 172–186. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 192–206. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  17. Hustadt, U., Schmidt, R.A.: A resolution decision procedure for fluted logic. Technical Report UMCS-00-3-1, University of Manchester, UK (2000)

    Google Scholar 

  18. Joyner Jr., W.H.: Resolution strategies as decision procedures. J. ACM 23(3), 398–417 (1976)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  20. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Computat. 2, 293–304 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  21. Purdy, W.C.: Decidability of fluted logic with identity. Notre Dame J. Formal Logic 37(1), 84–104 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  22. Purdy, W.C.: Fluted formulas and the limits of decidability. J. Symbolic Logic 61(2), 608–620 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  23. Purdy, W.C.: Surrogate variables in natural language. In: Böttner, M. (ed.) Proc. of the Workshop on Variable-Free Semantics (1996) (to appear)

    Google Scholar 

  24. Purdy, W.C.: Quine’s ‘limits of decision’. J. Symbolic Logic 64, 1439–1466 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  25. Quine, W.V.: Variables explained away. In: Proc. American Philosophy Society, vol. 104, pp. 343–347 (1960)

    Google Scholar 

  26. Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Automated Reasoning 22(4), 379–396 (1999)

    Article  MATH  Google Scholar 

  27. Tseitin, G.S.: On the complexity of derivations in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115–125, Consultants Bureau, New York (1970)

    Google Scholar 

  28. Weidenbach, C.: SPASS (1999), http://spass.mpi-sb.mpg.de

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Manchester, Manchester, M13 9PL, United Kingdom

    Renate A. Schmidt

  2. Centre for Agent Research and Development, Manchester Metropolitan University, Manchester, M1 5GD, United Kingdom

    Ullrich Hustadt

Authors
  1. Renate A. Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ullrich Hustadt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Toyota Technological Institute at Chicago, 1427 E. 60th Street, 60637, Chicago, Illinois

    David McAllester

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schmidt, R.A., Hustadt, U. (2000). A Resolution Decision Procedure for Fluted Logic. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_34

Download citation

  • DOI: https://doi.org/10.1007/10721959_34

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67664-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation