Although resolution-based inference is perhaps the industry standard in automated theorem proving, there have always been systems that employed a different format. For example, the Logic Theorist of 1957 produced proofs by using an axiomatic system, and the proofs it generated would be considered legitimate axiomatic proofs; Wang’s systems of the late 1950’s employed a Gentzen-sequent proof strategy; Beth’s systems written about the same time employed his semantic tableaux method; and Prawitz’s systems of again about the same time are often (...) said to employ a natural deduction format. [See Newell, et al (1957), Beth (1958), Wang (1960), and Prawitz et al (1960)]. Like sequent proof systems and tableaux proof systems, natural deduction systems retain.. (shrink)

A rational agent has beliefs reflecting the state of its environment, and likes or dislikes Its situation. When it finds the world not entirely to Its liking, it tries to change that. We can, accordingly, evaluate a system of cognition in terms of its probable success in bringing about situations that are to the agent's liking. In doing this we are viewing practical reasoning from “the design stance.” It is argued that a considerable amount of the structure of rationality can (...) be elicited as providing the only apporant solutions to various logical and feasibility problems that arise in the course of trying to design a rational agent that satisfies this design specification. (shrink)

Parmenides and Melissus employ different deductive styles for their different kinds of argumentation. The former’s poem flows in an interesting sequence of passages: contents foreword, methodological premises, krisis, conclusions and corollaries. The latter, however, organizes an extensive process of deduction to show the characteristics of what is. In both cases, the strength of their argument rests on their deductive form, on the syntactical level of their texts: the formal structure of their reasonings help to identify the features and logical intersections (...) of their thoughts. On the one hand, Parmenides uses modal reasoning, enforcing the employment of the principle of the excluded middle. On the other hand, Melissus radicalizes the use of modal reasoning and employs counterfactual statements in order to develop his doctrine of what is. Despite their differences, both deserve a place in the Stone Age of logic and theory of argumentation due to their common ambition to demonstrate what is. (shrink)