Skip to main content
SpringerLink
Log in

Automated Reasoning

  • Living reference work entry
  • First Online:
Encyclopedia of Social Network Analysis and Mining

  • 121 Accesses

Synonyms

Automated Deduction

Glossary

Backward chaining:

an inference method that searches backwards starting from the goal to be proven.

Complete:

a complete algorithm returns all correct answers (but may also return others).

Deduction calculus:

a formal system in mathematical logic to express logical derivations, i.e., proving that a conclusion can be inferred from a given set of assumptions.

Direct proof:

starts from the known assumptions, and proves the desired conclusion applying rules of inference in a step-wise manner.

Forward chaining:

an inference method that searches for solutions applying a set of inference rules to the available data.

Indirect proof:

assumes that the desired conclusion is wrong, and aims at proving that this together with the known information leads to a contradiction.

Resolution:

a rule of inference used to show that some goal/objective is not derivable.

SAT solver:

program that given a propositional formula returns whether it is satisfiable.

...

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

References

  • Baader F et al (eds) (2010) The description logic handbook: theory, implementation, and applications, 3rd edn. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  • Bibel W, Eder E (1993) Methods and calculi for deduction. In: Gabbay DM, Hogger CJ, Robinson JA (eds) Handbook of logic in artificial intelligence and logic programming, vol 1. Oxford University Press, New York, pp 68–182. http://dl.acm.org/citation.cfm?id=185728.185745

    Google Scholar 

  • Davis M (1983) The prehistory and early history of automated deduction. In: Siekmann J, Wrightson G (eds) Automation of reasoning. Classical papers on computational logic. Springer, Berlin, pp 1–28

    Google Scholar 

  • Davis M (2001) The early history of automated deduction: dedicated to the memory of Hao Wang. In: Robinson A, Voronkov A (eds) Handbook of automated reasoning. Elsevier, Amsterdam, pp 1–28

    Google Scholar 

  • Dowek G (2001) Higher-order unification and matching. In: Robinson A, Voronkov A (eds) Handbook of automated reasoning. Elsevier, Amsterdam, pp 1009–1062

    Chapter  Google Scholar 

  • Martin U, Pease A (2013) Mathematical practice, crowdsourcing, and social machines. In: Carette J, Aspinall D, Lange C, Sojka P, Windsteiger W (eds) Proceedings of intelligent computer mathematics – MKM, calculemus, DML, and systems and projects 2013, Held as Part of CICM 2013, Bath, 8–12 July 2013, Lecture notes in computer science, vol 7961. Springer, pp 98–119

    Google Scholar 

  • Portoraro F (2014) Automated reasoning. In: Zalta EN (ed) The stanford encyclopedia of philosophy, winter 2014 edn, http://plato.stanford.edu/archives/win2014/entries/reasoning-automated/

  • Robinson JA, Voronkov A (eds) (2001) Handbook of automated reasoning, 2 vols. Elsevier and MIT Press, Amsterdam

    Google Scholar 

Recommended Reading

  • Bibel W, Eder E (1993) is a detailed overview and comparison on many of the different deduction calculi

    Google Scholar 

  • Davis M (1983) presents an account on the early history of automated reasoning

    Google Scholar 

  • Portoraro F (2014) also provides a rather compact overview on the topic with further pointers to the literature

    Google Scholar 

  • Robinson A, Voronkov A (2001) describes exhaustively all aspects and major approaches to automated reasoning in a detailed manner

    Google Scholar 

  • The proceedings of the International Joint Conference on Automated Reasoning (IJCAR) and of the International Joint Conference on Automated Deducation (CADE) as well as the Journal of Automated Reasoning are the main venues for publication on automated reasoning

    Google Scholar 

Download references

Acknowledgments

The author acknowledges the support of FCT under strategic project NOVA LINCS (UID/CEC/04516/2013) and grant SFRH/BPD/86970/2012.

Author information

Authors and Affiliations

  1. NOVA LINCS and Dept. of Computer Science, Faculdade de Ciências e Tecnologia, Universidade NOVA de Lisboa, Quinta da Torre, 2829-516, Caparica, Portugal

    Matthias Knorr

Authors
  1. Matthias Knorr
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthias Knorr .

Editor information

Editors and Affiliations

  1. Computer Science, University of Calgary, Calgary, Alberta, Canada

    Reda Alhajj

  2. University of Calgary Computer Science, Calgary, Canada

    Jon Rokne

Section Editor information

  1. Institute for Web Science and Technologies, Universität Koblenz-Landau, Koblenz, Germany

    Thomas Gottron

  2. YU, Amsterdam, The Netherlands

    Stefan Schlobach

  3. Institute for Web Science and Technologies, Universität Koblenz-Landau, Koblenz, Germany

    Steffen Staab

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer Science+Business Media LLC

About this entry

Cite this entry

Knorr, M. (2017). Automated Reasoning. In: Alhajj, R., Rokne, J. (eds) Encyclopedia of Social Network Analysis and Mining. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-7163-9_110188-1

Download citation

  • DOI: https://doi.org/10.1007/978-1-4614-7163-9_110188-1

  • Received:

  • Accepted:

  • Published:

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4614-7163-9

  • Online ISBN: 978-1-4614-7163-9

  • eBook Packages: Springer Reference Computer SciencesReference Module Computer Science and Engineering

Publish with us

Policies and ethics

Search

Navigation