Title :
Correctness of multiplicative proof nets is linear
Author :
Guerrini, Stefano
Author_Institution :
Dipt. di Sci. dell´´Inf., Rome Univ., Italy
Abstract :
We reformulate Danos contractibility criterion in terms of a sort of unification. As for term unification, a direct implementation of the unification criterion leads to a quasi-linear algorithm. Linearity is obtained after observing that the disjoint-set union-find at the core of the unification criterion is a special case of union-find with a real linear time solution
Keywords :
formal logic; theorem proving; Danos contractibility; disjoint-set union-find; multiplicative proof nets; term unification; unification; Computer science; Ear; Educational institutions; Electrical capacitance tomography; Inspection; Linearity; Logic; Remuneration; Switches; Tree graphs;
Conference_Titel :
Logic in Computer Science, 1999. Proceedings. 14th Symposium on
Conference_Location :
Trento
Print_ISBN :
0-7695-0158-3
DOI :
10.1109/LICS.1999.782640
