A logic program P1 is said to be strongly equivalent to a logic program P2 if, for every logic program P, the union of P1 and P has the same answer sets as the union of P2 and P. The study of strong equivalence is important because we learn from it how we can simplify a part of a logic program without looking at the other parts. The logic of strong equivalence turns out to be identical to the 3-valued superintuitionistic logic called the logic of here-and-there. This is joint work with David Pearce and Agustin Valverde.
Feferman-Vaught theory of generalized products of algebraic systems is a very comprehensive framework about how to discover the first order properties of a complex system through analyzing the properties of its components.
We will briefly review the method of elimination of quantifiers which plays the central role in the proof of the basic composition theorem. Then we show that the notion of generalized product unifies a variety of ways of forming products in algebra and set theory. In particular, we show how the direct product, weak direct product, cardinal sum (direct sum) can be viewed as generalized products. Also the decidability of the theory of a product system reduces to the decidability of its factor systems and some certain subset algebras on the index set. Examples include the elementary theory of ordinal addition, cardinal addition and the theory of arithmetic with only multiplication.
We study proof systems for propositional formulas encoded by polynomial inequalities. These proof systems turn out to be rather strong: there are short semi-algebraic proofs of the propositional pigeon-hole principle, Tseitin's tautologies and other "hard" formulas. On the other hand, we are able to demonstrate exponential lower bounds on the proof size in some of these systems.
Usually one has to consider a relativized generalized direct product, whose carrier is a slight modification of a generalized product obtained by leaving out some components under some conditions. These conditions are described by simple set-theoretic formulas that take part in the decision procedure.
We describe in detail decision procedures for integer multiplication and ordinal addition. Soundness and completeness of these procedures rely on the following results.
Since Presburger arithmetic is decidable, so are both systems.
Time permitting, decidability of the theory of cardinal addition will be discussed.
A realizability interpretation for classical second order arithmetic is presented. This interpretation enables the extraction of witnessing polymorphic lambda terms from proofs of \Sigma^0_1 and \Pi^0_2 sentences. This realizability is constructed by applying the modified realizability for second order intuitionistic arithmetic to the result of a simple embedding of classical logic in intuitionistic logic, followed by the Friedman-Dragalin translation.