Group:
artificial intelligence
Topic:
logic programming
Topic:
mathematical proof
Topic:
string transformation languages
Topic:
symbolic execution
Topic:
symbolic manipulation of formulas
| |
Summary
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 
| 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
| 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
| 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
| 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
| 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
| 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
| 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
[»rabiMO8_1974]
|
Related Topics
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)
|
