Two preprints

--bcaec5158d8702077204d654da99
Content-Type: text/plain; charset=ISO-8859-1

Dear all,

I would like to advertise the following two preprints (abstracts below):

The pigeonhole principle and related counting arguments in weak monotone
systems
http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf

Rewriting with linear inferences in propositional logic
http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf

Any feedback would be greatly appreciated. I would also like to thank those
on this list who have already responded to preliminary versions of these
works for their helpful comments.

Kind regards,
Anupam


The pigeonhole principle and related counting arguments in weak monotone
systems

We construct quasipolynomial-size proofs of the propositional pigeonhole
principle for weak fragments of the monotone sequent calculus, implemented
in the simplest deep inference system for propositional logic. The argument
given, inspired by previous work on the monotone calculus, utilizes
propositional formulae that compute certain counting functions by providing
formal proofs of some basic properties. This is generalized to a natural
class of counting arguments, and can be applied to related classes of
propositional tautologies.
While we rely on much previous work in this area, this paper is essentially
self-contained, and we reference material where previous concepts and
results appear in more detail.


Rewriting with linear inferences in propositional logic

Linear inferences are sound implications of propositional logic where each
variable appears exactly once in the premiss and conclusion. We consider a
specific set of these inferences, MS, first studied by Strassburger,
corresponding to the logical rules in deep inference proof theory. Despite
previous results characterising the individual rules of MS, we show that
there is no polynomial-time characterisation of MS, assuming that integers
cannot be factorised in polynomial time.
We also examine the length of rewrite paths in MS, utilising a notion of
trivialisation to reduce the case with units to the case without, amongst
other observations on MS-rewriting and the set of linear inferences in
general.

--bcaec5158d8702077204d654da99
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable

Dear all,<div><br></div><div>I would like to advertise the following two pr=
eprints (abstracts below):</div><div><br></div><div>The pigeonhole principl=
e and related counting arguments in weak monotone systems</div><div><a href=
=3D"http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf">h=
ttp://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf</a></di=
v>
<div><br></div><div>Rewriting with linear inferences in propositional logic=
</div><div><a href=3D"http://www.anupamdas.com/items/RewritingWithLinearInf=
erences/RewritingWithLinearInferences.pdf">http://www.anupamdas.com/items/R=
ewritingWithLinearInferences/RewritingWithLinearInferences.pdf</a></div>
<div><br></div><div>Any feedback would be greatly appreciated. I would also=
 like to thank those on this list who have already responded to preliminary=
 versions of these works for their helpful comments.</div><div><br></div>
<div>Kind regards,</div><div>Anupam</div><div><br></div><div><br></div><div=
><div>The pigeonhole principle and related counting arguments in weak monot=
one systems</div><div><br></div><div>We construct quasipolynomial-size proo=
fs of the propositional pigeonhole principle for weak fragments of the mono=
tone sequent calculus, implemented in the simplest deep inference system fo=
r propositional logic. The argument given, inspired by previous work on the=
 monotone calculus, utilizes propositional formulae that compute certain co=
unting functions by providing formal proofs of some basic properties. This =
is generalized to a natural class of counting arguments, and can be applied=
 to related classes of propositional tautologies.</div>
<div>While we rely on much previous work in this area, this paper is essent=
ially self-contained, and we reference material where previous concepts and=
 results appear in more detail.</div></div><div><br></div><div><br></div>
<div><div>Rewriting with linear inferences in propositional logic</div><div=
><br></div><div>Linear inferences are sound implications of propositional l=
ogic where each variable appears exactly once in the premiss and conclusion=
. We consider a specific set of these inferences, MS, first studied by Stra=
ssburger, corresponding to the logical rules in deep inference proof theory=
. Despite previous results characterising the individual rules of MS, we sh=
ow that there is no polynomial-time characterisation of MS, assuming that i=
ntegers cannot be factorised in polynomial time.</div>
<div>We also examine the length of rewrite paths in MS, utilising a notion =
of trivialisation to reduce the case with units to the case without, amongs=
t other observations on MS-rewriting and the set of linear inferences in ge=
neral.</div>
</div>

--bcaec5158d8702077204d654da99--