Skip to main content
SpringerLink
Log in

Reduction Theorems for Boolean Formulas Using Δ-Trees

  • Conference paper
  • First Online:
Book cover Logics in Artificial Intelligence (JELIA 2000)

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

Included in the following conference series:

Abstract

A new tree-based representation for propositional formulas, named Δ-tree, is introduced. Δ-trees allow a compact representation for negation normal forms as well as for a number of reduction strategies in order to consider only those occurrences of literals which are relevant for the satisfiability of the input formula. These reduction strategies are divided into two subsets (meaning- and satisfiability-preserving transformations) and can be used to decrease the size of a negation normal form A at (at most) quadratic cost. The reduction strategies are aimed at decreasing the number of required branchings and, therefore, these strategies allow to limit the size of the search space for the SAT problem.

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

  1. G. Aguilera, I. P. de Guzmán, and M. Ojeda-Aciego. Increasing the efficiency of automated theorem proving. Journal of Applied Non-Classical Logics, 5(1):9–29, 1995.

    MATH  MathSciNet  Google Scholar 

  2. G. Aguilera, I. P. de Guzmán, M. Ojeda-Aciego, and A. Valverde. Reductions for non-clausal theorem proving. Theoretical Computer Science, 2000. To appear. Available at http://www.ctima.uma.es/aciego/TR/TAS-tcs.pdf.

  3. L.J. Claesen, editor. Formal VLSI correctness verification—VLSI design methods, volume 2. Elsevier, 1990.

    Google Scholar 

  4. I. P. de Guzmán, M. Ojeda-Aciego, and A. Valverde. Implicates and reduction techniques for temporal logics. Ann. Math. Artificial Intelligence 27:3–23, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  5. I. P. de Guzmán, M. Ojeda-Aciego, and A. Valverde. Multiple-valued tableaux with Δ-reductions. In Proc. of the Intl. Conf. on Artificial Intelligence, ICAI’99, pages 177–183. C.S.R.E.A., 1999.

    Google Scholar 

  6. J.H. Gallier. Logic for Computer Science: Foundations for Automatic Theorem Proving. Wiley & Sons, 1987.

    Google Scholar 

  7. F. Massacci. Simplification: a general constraint propagation technique for propositional and modal tableaux. In Proceedings of Tableaux’98, pages 217–231. Lect. Notes in Artificial Intelligence 1397, 1998.

    Google Scholar 

  8. L.C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.

    MATH  Google Scholar 

  9. P. W. Purdom, Jr. Average time for the full pure literal rule. Information Sciences, 78:269–291, 1994.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Matemática Aplicada, Universidad de Málaga, P.O. Box 4114, E-29080, Málaga, Spain

    Gloria Gutiérrez, Inma P. de Guzmán, Javier Martínez, Manuel Ojeda-Aciego & Agustín Valverde

Authors
  1. Gloria Gutiérrez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Inma P. de Guzmán
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Javier Martínez
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Manuel Ojeda-Aciego
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Agustín Valverde
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Applied Mathematics, E.T.S.I. Informática, University of Málaga, 29071, Málaga, Spain

    Manuel Ojeda-Aciego  & Inma P. de Guzmán  & 

  2. Intelligent Systems Department, Computer Science Institute, University of Leipzig, Augustusplatz 10-11, 04109, Leipzig, Germany

    Gerhard Brewka

  3. Center for Artificial Intelligence, Department of Computer Science, University of Lisbon, 2825-114, Caparica, Portugal

    Luís Moniz Pereira

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gutiérrez, G., de Guzmán, I.P., Martínez, J., Ojeda-Aciego, M., Valverde, A. (2000). Reduction Theorems for Boolean Formulas Using Δ-Trees. In: Ojeda-Aciego, M., de Guzmán, I.P., Brewka, G., Moniz Pereira, L. (eds) Logics in Artificial Intelligence. JELIA 2000. Lecture Notes in Computer Science(), vol 1919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40006-0_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-40006-0_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41131-4

  • Online ISBN: 978-3-540-40006-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation