The vision of machines autonomously carrying out substantive conjecture generation, theorem discovery, proof discovery, and proof verification in mathematics and the natural sciences has a long history that reaches back before the development of automatic systems designed for such processes. While there has been considerable progress in proof verification in the formal sciences, for instance the Mizar project’ and the four-color theorem, now machine verified, there has been scant such work carried out in the realm of the natural sciences—until recently. (...) The delay in the case of the natural sciences can be attributed to both a lack of formal analysis of the so-called “theories” in such sciences, and the lack of sufficient progress in automated theorem proving. While the lack of analysis is probably due to an inclination toward informality and empiricism on the part of nearly all of the relevant scientists, the lack of progress is to be expected, given the computational hardness of automated theorem proving; after all, theoremhood in even first-order logic is Turing-undecidable. We give in the present short paper a compressed report on our building upon these formal theories using logic-based AI in order to achieve, in relativity, both machine proof discovery and proof verification, for theorems previously established by humans. Our report is intended to serve as a springboard to machine-produced results in the future that have not been obtained by humans. (shrink)

Knowledge Representation and Reasoning (KR&R) is based on the idea that propositional content can be rigorously represented in formal languages long the province of logic, in such a way that these representations can be productively reasoned over by humans and machines; and that this reasoning can be used to produce knowledge-based systems (KBSs). As such, KR&R is a discipline conventionally regarded to range across parts of artificial intelligence (AI), computer science, and especially logic. This standard view of KR&R’s participating fields (...) is correct — but dangerously incomplete. The view is incomplete because, as we explain herein, sophisticated KR&R must rely heavily upon philosophy. Encapsulated, the reason is actually quite straightforward: Sophisticated KR&R must include the representation of not only simple properties, but also concepts that are routine in the formal sciences (theoretical computer science, mathematics, logic, game theory, etc.), and everyday socio-cognitive concepts like mendacity, deception, betrayal, and evil. Because in KR&R the representation of such concepts must be rigorous in order to enable machine reasoning (e.g., machine-generated and machine-checked proofs that a is lying to b) over them, philosophy, devoted as it is in no small part to supplying analyses of such concepts, is a crucial partner in the overall enterprise. To put the point another way: When the knowledge to be represented is such as to require lengthy formulas in expressive formal languages for that representation, philosophy must be involved in the game. In addition, insofar as the advance of KR&R must allow formalisms and processes for representing and reasoning over visual propositional content, philosophy will be a key contributor into the future. (shrink)

An illustrated beginner's guide to the visual arts examines specific art works, studies expression and construction of art, and discusses creative and technical processes of art.

As some artists discovered early in the century, there is a particular pleasure and stimulation to be derived from works of art created by cultures untouched by our own traditions of form. In part this is probably a delight in exoticism, in being away from home, and in part it possibly is our sentiment for cultures we look on as traditional, in a Jungian sense, or primitive in their unquestioning allegiance to simple cultural necessity. But more significantly, without indulging in (...) philosophical or anthropological speculation, we are forced, in looking at such objects as these elegantly designed boxes and bowls, to revise our visual thinking, our assumptions about unity and grace.Joshua C. Taylor, director of the National Collection of Fine Arts of the Smithsonian Institution, has written Learning to Look, William Page: The American Titian, and catalogues of exhibits of futurism and the works of Umberto Boccioni. Part 1 of this paper has been published in somewhat different form in Boxes and Bowls. (shrink)