Propositional proof complexity is the study of the sizes of propositional proofs, and more generally, the resources necessary to certify propositional tautologies. Questions about proof sizes have connections with computational complexity, theories of arithmetic, and satisfiability algorithms. This is article includes a broad survey of the field, and a technical exposition of some recently developed techniques for proving lower bounds on proof sizes.

Representation of scientific knowledge in ontologies suffers so often from the lack of computational knowledge required for inference. This article aims to perform quantitative analysis on physical systems, that is, to answer questions about values of quantitative state variables of a physical system with known structure. For this objective, we incorporate procedural knowledge on two distinct levels. At the domain-specific level, we propose a representation model for scientific knowledge, i.e. variables, theories, and laws of nature. At the domain-independent level, we (...) provide an algorithm which, given a system S with known structure and a relevant scientific theory T, extracts a constraint network, whose variables are state variables of S defined by T, and whose constraints raise from relevant laws in T. The constraint network is then solved, to build a system of equations whose unknowns are the output variables of S. The proposed representation model and reasoning algorithm are evaluated by applying them to classic analysis examples. (shrink)

A new theory of problem solving is presented, which embeds problem solving in the theory of action; in this theory, a problem is just a difficult action. Making this work requires a sophisticated language for‐talking about plans and their execution. This language allows a broad range of types of action, and can also be used to express rules for choosing and scheduling plans. To ensure flexibility, the problem solver consists of an interpreter driven by a theorem prover which actually manipulates (...) formulas of the language. Many examples of the use of the system six given. including an extended treatment of the world of blocks. Limitations and extensions of the system are discussed at length. It is concluded that a rule‐based problem solver is necessary and feasible, but that much more work remains to be done on the underlying theory of planning and acting. (shrink)

In the wake of Frege's attack on psychologism and the subsequent influence of Logical Positivism, psychological considerations in philosophy came to be viewed with suspicion. Philosophical questions, especially epistemological ones, were viewed as 'logical' questions, and logic was sharply separated from psychology. Various efforts have been made of late to reconnect epistemology with psychology. But there is little agreement about how such connections should be made, and doubts about the place of psychology within epistemology are still much in evidence. It (...) therefore remains to be clarified just how such links should be established, and what impact they would have on the direction of epistemology. (shrink)