-
Enumerating All Maximal Clique-Partitions of an Undirected Graph
Authors:
Mircea Marin,
Temur Kutsia,
Cleo Pau,
Mikheil Rukhaia
Abstract:
We address the problem of enumerating all maximal clique-partitions of an undirected graph and present an algorithm based on the observation that every maximal clique-partition can be produced from the maximal clique-cover of the graph by assigning the vertices shared among maximal cliques, to belong to only one clique. This simple algorithm has the following drawbacks: (1) the search space is ver…
▽ More
We address the problem of enumerating all maximal clique-partitions of an undirected graph and present an algorithm based on the observation that every maximal clique-partition can be produced from the maximal clique-cover of the graph by assigning the vertices shared among maximal cliques, to belong to only one clique. This simple algorithm has the following drawbacks: (1) the search space is very large; (2) it finds some clique-partitions which are not maximal; and (3) some clique-partitions are found more than once. We propose two criteria to avoid these drawbacks. The outcome is an algorithm that explores a much smaller search space and guarantees that every maximal clique-partition is computed only once. The algorithm can be used in problems such as anti-unification with proximity relations or in resource allocation tasks when one looks for several alternative ways to allocate resources.
△ Less
Submitted 24 September, 2023;
originally announced September 2023.
-
Advanced Proof Viewing in ProofTool
Authors:
Tomer Libal,
Martin Riener,
Mikheil Rukhaia
Abstract:
Sequent calculus is widely used for formalizing proofs. However, due to the proliferation of data, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but since they normally utilize Gentzen's original notation, some of the problems persist. In this paper, we introduce a number of criteria for proof visualization wh…
▽ More
Sequent calculus is widely used for formalizing proofs. However, due to the proliferation of data, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but since they normally utilize Gentzen's original notation, some of the problems persist. In this paper, we introduce a number of criteria for proof visualization which we have found out to be crucial for analyzing proofs. We then evaluate recent developments in tree visualization with regard to these criteria and propose the Sunburst Tree layout as a complement to the traditional tree structure. This layout constructs inferences as concentric circle arcs around the root inference, allowing the user to focus on the proof's structural content. Finally, we describe its integration into ProofTool and explain how it interacts with the Gentzen layout.
△ Less
Submitted 29 October, 2014;
originally announced October 2014.
-
PROOFTOOL: a GUI for the GAPT Framework
Authors:
Cvetan Dunchev,
Alexander Leitsch,
Tomer Libal,
Martin Riener,
Mikheil Rukhaia,
Daniel Weller,
Bruno Woltzenlogel-Paleo
Abstract:
This paper introduces PROOFTOOL, the graphical user interface for the General Architecture for Proof Theory (GAPT) framework. Its features are described with a focus not only on the visualization but also on the analysis and transformation of proofs and related tree-like structures, and its implementation is explained. Finally, PROOFTOOL is compared with three other graphical interfaces for proofs…
▽ More
This paper introduces PROOFTOOL, the graphical user interface for the General Architecture for Proof Theory (GAPT) framework. Its features are described with a focus not only on the visualization but also on the analysis and transformation of proofs and related tree-like structures, and its implementation is explained. Finally, PROOFTOOL is compared with three other graphical interfaces for proofs.
△ Less
Submitted 8 July, 2013;
originally announced July 2013.
-
CERES for First-Order Schemata
Authors:
Cvetan Dunchev,
Alexander Leitsch,
Mikheil Rukhaia,
Daniel Weller
Abstract:
The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is always unsatisfiable. A resolution refutation of this clause set can be used as a skeleton for a proof with atomic cuts only (atomic cut normal form). This is achieved by replacing clauses from the resolution refutation by…
▽ More
The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is always unsatisfiable. A resolution refutation of this clause set can be used as a skeleton for a proof with atomic cuts only (atomic cut normal form). This is achieved by replacing clauses from the resolution refutation by the corresponding projections of the original proof.
We present a generalization of CERES (called CERESs) to first-order proof schemata and define a schematic version of the sequent calculus called LKS, and a notion of proof schema based on primitive recursive definitions. A method is developed to extract schematic characteristic clause sets and schematic projections from these proof schemata. We also define a schematic resolution calculus for refutation of schemata of clause sets, which can be applied to refute the schematic characteristic clause sets. Finally the projection schemata and resolution schemata are plugged together and a schematic representation of the atomic cut normal forms is obtained. A major benefit of CERESs is the extension of cut-elimination to inductively defined proofs: we compare CERESs with standard calculi using induction rules and demonstrate that CERESs is capable of performing cut-elimination where traditional methods fail. The algorithmic handling of CERESs is supported by a recent extension of the CERES system.
△ Less
Submitted 18 March, 2013;
originally announced March 2013.
