Topic: theorem proving systems

topics > computer science > programming > Group: program proving

artificial intelligence

logic programming
mathematical proof
string transformation languages
symbolic execution
symbolic manipulation of formulas


Automated theorem proving is an important branch of artificial intelligence. Theorems, located in a database, are defined in an abstract language. New theorems are proved by a goal-oriented pattern transformation search. Heuristics and other AI techniques are heavily used. (cbb 5/80)
Subtopic: interactive proof up

Quote: need interactive system for effective theorem proving; users provide strategy and insights, computers do the calculations [»rushJ12_1991]
Quote: using an interactive proof system produced a publishable proof, enumeration of all assumptions, and exploration of changed assumptions [»rushJ12_1991]
Quote: an interactive proof should produce a publishable proof and a robust, strategy for automating the proof [»rushJ12_1991]
Quote: an automatic theorem prover may be worse; no human review and no help with discovering proof errors; should automate calculations, etc. [»rushJ12_1991]

Subtopic: examples of interactive proof up

Quote: proof of type soundness for a large, sequential sublanguage of Java; via the interactive theorem prover Isabelle/HOL [»nipkT1_1998]
Quote: semiautomatically derive sample behavioral models from the TRIO specification of a system [»ciapE1_1999]
Quote: semiautomatic proof of temporal theorems from TRIO axioms [»ciapE1_1999]

Subtopic: theorem prover as skeptic up

Quote: a theorem prover acts as an implacable skeptic that insists on stated assumptions and justified claims; not an oracle [»rushJ12_1991]

Subtopic: proof and assertion database up

Quote: a proof is a set of correct assertions; use a proof system to keep track of proved and unproved assertions [»pratVR_1980]

Subtopic: theory representation up

QuoteRef: bursRM8_1977 ;;1047 a theory presentation is specified sorts [or objects], named operations on sorts returning sorts, equations relating the operations and sorts.
QuoteRef: bobrDG9_1974 ;;167 planner: theorems part of data base. consist of pattern to be tested by a program which generally consists of other pattern tests.
QuoteRef: bobrDG9_1974 ;;167 theorem to build resultant data items from a new datum (antecedent)
QuoteRef: bobrDG9_1974 ;;167 theorems for goal oriented searches e.g., consequent (part $?x $?z) [this is a pattern] (goal (part $?x $?y)) (goal (part $?Y $?z)) tests for transitivity in data base.
QuoteRef: bobrDG9_1974 ;;167 theorems to delete corresponding data [derived data relationships] whenever a datum is deleted (erase, opposite of antecedent)

Subtopic: examples of theorem provers up

Quote: Larch shared and interface languages for incremental construction of readable specifications from other specifications; includes theorem prover for semantic checking [»guttJV9_1985]
Quote: used the theorem prover HOL to prove the correctness of SPIN's partial order reduction
Quote: SD3 extends datalog by associating names with authenticated public keys, e.g., T(x,y):-K$E(x,y) holds if E(x,y) and relation E under keyholder of K [»jimT5_2000]

Subtopic: automated proof as too long up

Quote: there are always short true statements concerning the addition of natural numbers whose formal proof is super-exponentially long [»rabiMO8_1974]
Quote: Rabin's proofs only disprove the feasibility of theorem-proving systems and combinatorially complex data correlations; already abandoned by most of AI [»carbJG3_1978]
Quote: proofs with a general purpose theorem prover may almost always be impractically long

Related Topics up

Group: artificial intelligence   (14 topics, 509 quotes)

Topic: logic programming (34 items)
Topic: mathematical proof (23 items)
Topic: string transformation languages (17 items)
Topic: symbolic execution (9 items)
Topic: symbolic manipulation of formulas
(12 items)

Updated barberCB 2/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.