# Category:Automated theorem proving

Computing portal |

Here is a list of articles in the Automated theorem proving category of the Computing portal that unifies foundations of mathematics and computations using computers.

## Subcategories

This category has the following 2 subcategories, out of 2 total.

## Pages in category "Automated theorem proving"

The following 36 pages are in this category, out of 36 total.

- Automated theorem proving
*(computing)*

### A

- Anti-unification (computer science)
*(computing)* - Automated reasoning
*(computing)*

### B

- Burrows–Abadi–Needham logic
*(computing)*

### C

- Chaff algorithm
*(computing)* - Computer-assisted proof
*(computing)* - Concolic testing
*(computing)*

### D

- Davis–Putnam algorithm
*(computing)* - DPLL algorithm
*(computing)* - DPLL(T)
*(computing)*

### F

- F* (programming language)
*(computing)*

### G

- Harald Ganzinger
*(computing)* - Geometry Expert
*(computing)*

### H

- Hilbert system
*(computing)*

### I

- IsaPlanner
*(computing)*

### L

- LowerUnits
*(computing)*

### M

- Method of analytic tableaux
*(computing)* - Model elimination
*(computing)*

### N

- Non-surveyable proof
*(computing)* - Nuprl
*(computing)*

### O

- Occurs check
*(computing)*

### P

- Proof (truth)
*(computing)* - Proof assistant
*(computing)* - Proof complexity
*(computing)* - Propositional proof system
*(computing)*

### R

- Reasoning system
*(computing)* - Resolution (logic)
*(philosophy)* - Rippling
*(computing)*

### S

- Sequent calculus
*(computing)* - Substitution (logic)
*(philosophy)* - System on TPTP
*(computing)*

### T

- Interactive Theorem Proving (conference)
*(computing)* - Thousands of Problems for Theorem Provers
*(computing)*

### U

- Unification (computer science)
*(computing)* - Unit propagation
*(computing)*

### W

- WalkSAT
*(computing)*