Abstract
After a brief history and motivation of Automated Deduction (AD), the necessary notions of first order logic are defined and different aspects of the Superposition calculus and semantic tableaux are presented. This last method can be suitably adapted to non classical logics, as illustrated by a few examples. The issues connected to incompleteness of mathematics are then addressed. By lack of space a number of issues and recent developments are only alluded to, either by name or through references to a succinct bibliography.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
At least one constant is assumed to exist in \(\mathscr {F}\), so that \(\varSigma (\emptyset ,\mathscr {F})\ne \emptyset \).
- 2.
See Sect. 3.2.
- 3.
I.e., if there exists an interpretation satisfying every formula in the branch.
- 4.
Either because the signature contains a function symbol or arity strictly greater than 0, or because new constants are repeatedly created by the \(\delta \) rule.
- 5.
If \(x ~ R~ y \in \mathscr {B}\) then \(x\in \mathscr {B}_E\) and \(y\in \mathscr {B}_E\), according to the rules.
References
Barendregt H, Wiedijk F (2005) The challenge of computer mathematics. Philos Trans R Soc A 363:2351–2375
Berardi S, Tatsuta M (2017) Equivalence of inductive definitions and cyclic proofs under arithmetic. In: 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavik, Iceland, 20–23 June 2017. IEEE Computer Society, pp 1–12
Blanchette JC, Fleury M, Lammich P, Weidenbach C (2018) A verified SAT solver framework with learn, forget, restart, and incrementality. J Autom Reason 61(1–4):333–365
Bledsoe WW, Loveland DW (eds) (1984) Automated theorem proving: after 25 years. Contemporary mathematics, vol 29. American Mathematical Society, Providence
Buss SR (1998) Handbook of proof theory. Studies in logic and the foundations of mathematics. Elsevier Science Publisher, New York
Caferra R, Leitsch A, Peltier N (2004) Automated model building. Applied logic (Kluwer), vol 31. Springer (Kluwer), Berlin
de Moura LM, Kong S, Avigad J, van Doorn F, von Raumer J (2015) The lean theorem prover (system description). In: Automated deduction - CADE-25 - 25th international conference on automated deduction, Berlin, Germany, 1–7 August 2015, Proceedings, pp 378–388
Fitting MC (1983) Proof methods for modal and intuitionistic logics, vol 169. Synthese library. D. Reidel, Dordrecht
Fitting MC (1996) First-order logic and automated theorem proving, 2nd edn. Springer, New York
Goré R (1999) Tableau methods for modal and temporal logics. Handbook of tableau methods. Kluwer Academic Publishers, Dordrecht, pp 297–396
Kripke SA (1963) Semantical analysis of modal logic I, normal propositional calculi. Zeitschr f math Logik u Grundl d Math 9:67–96
Leitsch A (1997) The resolution calculus. Texts in theoretical computer science. Springer, Berlin
Massacci F (2000) Single step tableaux for modal logics. J Autom Reason 24(3):319–364
Reynolds A, Blanchette JC, Cruanes S, Tinelli C (2016) Model finding for recursive functions in SMT. In: Automated reasoning - 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27–July 2 2016, Proceedings, pp 133–151
Robinson JA, Voronkov A (2001) Handbook of automated reasoning (2 volumes). Elsevier and MIT Press, Amsterdam and Cambridge
Schütte P (1978) Vollständige Systeme modaler und intuitionistischer Logik. Springer, Berlin
Siekmann J, Wrightson G (eds) (1983) Automation of reasoning. Classical papers on computational logic 1957-1967 and 1967-1970, vol 1, 2. Springer, Berlin
Sloman A (2008) The well-designed young mathematician. Artif Intell 172(18):2015–2034
Sutcliffe G (2017) The TPTP problem library and associated infrastructure - from CNF to th0, TPTP v6.4.0. J Autom Reason 59(4):483–502
Wos L (1988) Automated reasoning: 33 basic research problems. Prentice Hall, Englewood Cliffs
Wos L, Overbeek R, Lusk E, Boyle J (1992) Automated reasoning: introduction and applications. McGraw-Hill, New York
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Boy de la Tour, T., Caferra, R., Olivetti, N., Peltier, N., Schwind, C. (2020). Automated Deduction. In: Marquis, P., Papini, O., Prade, H. (eds) A Guided Tour of Artificial Intelligence Research. Springer, Cham. https://doi.org/10.1007/978-3-030-06167-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-06167-8_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-06166-1
Online ISBN: 978-3-030-06167-8
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)