Two papers on models of classical proofs, both at http://www.cs.bath.ac.uk/~pym/recent.html -- A combinatorial model of classical proofs. David Pym, Eike Ritter, and Edmund Robinson. Abstract. We present a combinatorial model of classical proofs that correctly models cut-elimination. The model is based on certain relations between propositional literals. The model is non-trivial (hom-sets are not singletons), non-compact (conjunction and disjunction are distinguished) instance of F=FChrmann and Pym's classical categories. We establish a one-to-one correspondence between elements of our model and proofs obtained by the connection (or matrix) method of Andrews, Bibel, and Wallen that arises in automated theorem proving. Submitted, 2005. -- A games semantics for proofs in the classical sequent calculus. David Pym, Eike Ritter, and Carsten F=FChrmann. Abstract. We present a games semantics for proofs in the classical sequent calculus that correctly models cut-elimination. Our semantics, inspired by ideas from reductive logic and proof-search, yields a non-trivi= al, non-compact example of F=FChrmann and Pym's categorical models of classical proofs. As a corollary, we obtain a MIX-free games semantics for multiplicative linear logic. Submitted, 2005. -- Thanks, David --=20 Prof. David J. Pym Telephone: +44 (0)1 225 38 3246 Professor of Logic & Computation Facsimile: +44 (0)1 225 38 3493 University of Bath Email: d.j.pym@bath.ac.uk Bath BA2 7AY, England, U.K. Web: http://www.bath.ac.uk/~cssdjp Royal Society Industry Fellow, HP Labs, Bristol: david.pym@hp.com 15-Apr-2005 11:54:45 -0300,1259;000000000001-0000000a