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 goaloriented 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 superexponentially long [»rabiMO8_1974]
 Quote: Rabin's proofs only disprove the feasibility of theoremproving 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)
