Short proofs for tricky formulas
type: Item
instance of: scholarly article
title: Short proofs for tricky formulas
zbMATH Open document ID: 0552.03009
DOI: 10.1007/BF00265682
author: Balakrishnan Krishnamurthy
published in: Acta Informatica
publication date: 1985-01-01T00:00:00Z
review text: The object of this paper is to demonstrate how certain tricky mathematical arguments can be encoded as short formal proofs for the propositional tautologies representing the mathematical statements. Using resolution as a base proof system for the propositional calculus, we exhibit these short proofs under resolution augmented by one of two principles: the principle of extension, originally suggested by Tseitin, and the principle of symmetry, introduced in this paper. These short proofs illustrate the power of extension and symmetry in theorem proving. The principle of extension allows the introduction of auxiliary variables to represent intermediate formulas so that the length of a proof can be significantly reduced by manipulating these variables instead of the formulas that they stand for. Symmetry, on the other hand, allows one to recognize that a tautology remains invariant under certain permutations of variable names, and use that information to avoid repeated independent derivations of intermediate formulas that are merely permutational variants of one another. First we show that a number of inductive arguments can be encoded as short formal proofs using either extension or symmetry. We provide the details for the tautologies derived by encoding the statement, ''An acyclic digraph on n vertices must have a source.'' We then consider the familiar checkerboard puzzle which asserts that a checkerboard, two of whose diagonally opposite corner squares are removed, cannot be perfectly covered with dominoes. We demonstrate short proofs for the tautologies derived from the above assertion, using extension to mimic the tricky informal argument. Finally, we consider statements asserting the Ramsey property of numbers much larger than the critical Ramsey numbers. We show that the proof of Ramsey's theorem can be imitated using the principle of symmetry to yield short proofs for these tautologies. The main theme of the paper is that both extension and symmetry are very po…
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 3878893
zbMATH Keywords: formal proofs
zbMATH Keywords: propositional tautologies
zbMATH Keywords: resolution
zbMATH Keywords: propositional calculus
zbMATH Keywords: symmetry
zbMATH Keywords: extension
zbMATH Keywords: inductive arguments
zbMATH Keywords: acyclic digraph
zbMATH Keywords: checkerboard puzzle
zbMATH Keywords: Ramsey numbers
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00265682
OpenAlex ID: W1999522767
description: scientific article; zbMATH DE number 3878893