Advantages
For automated theorem proving condensed detachment has a number of advantages over raw modus ponens and uniform substitution.
At a Modus Ponens and substitution proof you have an infinite number of choices for what you can substitute for variables. This means that you have an infinite number of possible next steps. With condensed detachment there are only a finite number of possible next steps in a proof.
The D-notation for complete condensed detachment proofs allows easy description of proofs for cataloging and search. A typical complete 30 step proof is less than 60 characters long in D-notation (excluding the statement of the axioms.)
Read more about this topic: Condensed Detachment
Famous quotes containing the word advantages:
“In 1845 he built himself a small framed house on the shores of Walden Pond, and lived there two years alone, a life of labor and study. This action was quite native and fit for him. No one who knew him would tax him with affectation. He was more unlike his neighbors in his thought than in his action. As soon as he had exhausted himself that advantages of his solitude, he abandoned it.”
—Ralph Waldo Emerson (1803–1882)
“Can you conceive what it is to native-born American women citizens, accustomed to the advantages of our schools, our churches and the mingling of our social life, to ask over and over again for so simple a thing as that “we, the people,” should mean women as well as men; that our Constitution should mean exactly what it says?”
—Mary F. Eastman, U.S. suffragist. As quoted in History of Woman Suffrage, vol. 4 ch. 5, by Susan B. Anthony and Ida Husted Harper (1902)
“If the minds of women were enlightened and improved, the domestic circle would be more frequently refreshed by intelligent conversation, a means of edification now deplorably neglected, for want of that cultivation which these intellectual advantages would confer.”
—Sarah M. Grimke (1792–1873)