Automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.
- Comment
- enAutomated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.
- Has abstract
- enAutomated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.
- Hypernym
- Subfield
- Is primary topic of
- Automated theorem proving
- Label
- enAutomated theorem proving
- Link from a Wikipage to an external page
- www.mathapplets.net/Programs/Meta%20Theorem/
- vprover.github.io/licence.html
- www.cis.upenn.edu/~jean/gbooks/logic.html
- logictools.org
- gtps.math.cmu.edu/cgi-bin/tpsdist.pl
- github.com/johnyf/tool_lists/blob/master/verification_synthesis.md%23theorem-provers
- Link from a Wikipage to another Wikipage
- ACL2
- Acumen RuleManager
- Alan Turing
- Alfred North Whitehead
- Allen Newell
- Alonzo Church
- Alt-Ergo
- AMD
- Argonne National Laboratory
- Aristotelian logic
- Automated reasoning
- Automath
- Baden-Württemberg Cooperative State University
- Begriffsschrift
- Bertrand Russell
- Binary decision diagram
- BSD License
- BSD Licenses
- CADE ATP System Competition
- CARINE
- Category:Automated theorem proving
- Category:Formal methods
- Cliff Shaw
- Completeness (logic)
- Computability
- Computer-aided proof
- Computer algebra system
- Computer program
- Computer science
- Connect Four
- Co-NP-complete
- Curry–Howard correspondence
- CVC (theorem prover)
- David Luckham
- Decidability (logic)
- Disjunctive normal form
- DPLL algorithm
- Eclipse (software)
- Elsevier
- Equational prover
- E theorem prover
- First-order logic
- First-order resolution
- Floating point unit
- Formal verification
- Four color theorem
- FreeBSD license
- Freeware
- General Problem Solver
- GKC Theorem Prover
- Gödel's completeness theorem
- Gödel's incompleteness theorem
- Gödel machine
- Gottlob Frege
- GPL
- Herbert A. Simon
- Herbrand interpretation
- Herbrand universe
- Higher-order logic
- Institute for Advanced Study
- Integrated circuit design
- Intel
- IsaPlanner
- Jape (software)
- Java Webstart
- John Alan Robinson
- JOHNNIAC
- KED theorem prover
- KeY
- Kurt Gödel
- LCF (theorem prover)
- LeanCoP
- Leo II (theorem prover)
- Leopold Löwenheim
- LGPL
- Logicism
- Logic programming
- Logic Theory Machine
- LoTREC
- Löwenheim–Skolem theorem
- Mace4
- Martin Davis (mathematician)
- Mathematical induction
- Mathematical logic
- Mathematical proof
- Mathematical theorem
- Max Planck Institute for Computer Science
- McGraw–Hill
- Metamath
- MetaPRL
- Method of analytic tableaux
- MIT License
- MIT Press
- Mizar system
- Model checking
- Model elimination
- Modus ponens
- Mojżesz Presburger
- Mozilla Public License
- Natural numbers
- Non-surveyable proofs
- NuPRL
- On Formally Undecidable Propositions of Principia Mathematica and Related Systems
- Otter (theorem prover)
- Paradox (theorem prover)
- Paramodulation
- Peano axioms
- Pentium FDIV bug
- PhoX
- Predicate logic
- Presburger arithmetic
- Primitive recursive function
- Principia Mathematica
- Program analysis (computer science)
- Program verification
- Proof assistant
- Proof checking
- Proof complexity
- Proof compression
- Proof verification
- Propositional formula
- Propositional logic
- Prototype Verification System
- Prover9
- ProverBox
- Prover Plug-In
- Ramanujan machine
- Recursively enumerable
- ResearchCyc
- Resolution (logic)
- Rewriting
- Robbins conjecture
- SETHEO
- Simplify (software)
- SNARK theorem prover
- SPARK (programming language)
- SPASS
- Spear modular arithmetic theorem prover
- Stanford University
- Strftime
- Stuttgart
- Superposition calculus
- Symbolic computation
- System on TPTP
- Technical University of Munich
- The Foundations of Arithmetic
- Theorem Proving System
- Thoralf Skolem
- Twelf
- Unification (computing)
- University of Manchester
- Validity (logic)
- Vampire theorem prover
- Well-formed formula
- Wolfgang Bibel
- Wolfram Mathematica
- World War II
- Z3 Theorem Prover
- SameAs
- 2Pqw2
- Automated theorem proving
- Automatyczne dowodzenie twierdzeń
- Demonstração Automatizada de Teoremas
- Démonstration automatique de théorèmes
- Demostración automática de teoremas
- Dimostrazione automatica di teoremi
- m.0 8m
- Otomatik teorem kanıtlama
- Prova automática de teoremas
- Q25427593
- Q431667
- Teoremen frogapen automatiko
- Teoremlərin avtomatik sübutu
- Автоматизоване доведення теорем
- Автоматическое доказательство
- Թեորեմների ավտոմատացված ապացուցում
- اثبات قضیه خودکار
- การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์
- 自動化定理證明
- 自動定理証明
- 자동 정리 증명
- SeeAlso
- Proof assistant
- Subject
- Category:Automated theorem proving
- Category:Formal methods
- WasDerivedFrom
- Automated theorem proving?oldid=1122886342&ns=0
- WikiPageLength
- 28124
- Wikipage page ID
- 2546
- Wikipage revision ID
- 1122886342
- WikiPageUsesTemplate
- Template:Anchor
- Template:Authority control
- Template:Citation needed
- Template:Cite book
- Template:Colend
- Template:Div col
- Template:Dts
- Template:Dunno
- Template:GBurl
- Template:ISBN
- Template:Mathematical logic
- Template:More citations needed section
- Template:No
- Template:Refbegin
- Template:Refend
- Template:Reflist
- Template:See also
- Template:Short description
- Template:Small
- Template:Unreferenced section
- Template:Yes