commit b8d10963826bb02cc0a250c7ac5f5d381b25bc0b
parent fafe2f80ff2cafa6d534f172c970a76ddbb828bf
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Tue, 14 Apr 2026 18:21:38 +0200
commit with codex
Diffstat:
12 files changed, 43 insertions(+), 15 deletions(-)
diff --git a/boolean_function b/boolean_function
@@ -16,6 +16,9 @@ Notions:
- [boolean_valuation]
- [satisfying_valuation]
- [falsifying_valuation]
+- [decision_tree]
+ - [instance_complexity]
+ - [decision_tree_complexity]
Representations:
diff --git a/crossing_number b/crossing_number
@@ -8,6 +8,8 @@ An [undirected_graph] is a [planar_graph] iff the crossing number is zero
[crossing_number_inequality]
+[crossing_number_computation]
+
The crossing number of [complete_bipartite_graphs] is an [open_problem], cf https://en.wikipedia.org/wiki/Tur%C3%A1n%27s_brick_factory_problem
Up: [planar_graph]
diff --git a/decision_tree b/decision_tree
@@ -2,9 +2,10 @@
A way to represent a [Boolean_function]
-Generalization: [bdd]
+Generalization: [BDD]
-The [boolean_function_equivalence] problem on decision trees can be solved in [quadratic] time, cf [cockett1987discrete] and [zantema1998equivalence]
+- [decision_tree_equivalence]
+- [decision_tree_complexity]
Up: [knowledge_compilation_formalisms]
diff --git a/decision_tree_equivalence b/decision_tree_equivalence
@@ -0,0 +1,5 @@
+# Decision tree equivalence
+
+The [boolean_function_equivalence] problem on decision trees can be solved in [quadratic] time, cf [cockett1987discrete] and [zantema1998equivalence]
+
+Up: [decision_tree], [equivalence_problem]
diff --git a/dsdnnf b/dsdnnf
@@ -1,11 +1,13 @@
# d-SDNNF
-[structuredness] [deterministic] [decomposable] [circuit]
+[structured_circuit] [deterministic] [decomposable] [circuit]
not closed under [complementation], cf [vinallsmeeth2024structured] by [harry]
- [dSDNNF_lower_bounds]
+Restriction: [TDDs], cf [capelli2026canonical]
+
Up: [knowledge_compilation_classes], [ddnnf], [sdnnf]
Aliases: dSDNNFs, d_SDNNFs, d_SDNNF
diff --git a/guarded_second_order_logic b/guarded_second_order_logic
@@ -0,0 +1,11 @@
+# Guarded second order logic
+
+A variant of [second_order_logic] where quantification is semantically restricted to only apply to [guarded_tuples]
+
+See [gradel2002back]
+
+Up: [monadic_second_order_logic]
+
+Aliases: GSO
+
+See also: [MSO2]
diff --git a/instance_complexity b/instance_complexity
@@ -0,0 +1,9 @@
+# Instance complexity
+
+studied in [liu2026instance] for [Boolean_functions]
+
+Relates to the [certificate_complexity] and [decision_tree_complexity]
+
+Up: [boolean_function]
+
+See also: [instance_optimal]
diff --git a/monadic_second_order_logic b/monadic_second_order_logic
@@ -11,6 +11,7 @@ Extensions:
- [counting_monadic_second_order_logic]
- [weighted_MSO]
+- [guarded_second_order_logic]
[Computational_complexity]:
diff --git a/monadic_second_order_logic_2 b/monadic_second_order_logic_2
@@ -1,11 +0,0 @@
-# Monadic second order logic 2
-
-also called "incidence encoding", corresponds to the [incidence_graph] between [vertices] and [edges]
-
-Can express that a [graph] has a [Hamiltonian_cycle], [max_cut], [edge_dominating_set], [graph_coloring]
-
-Up: [monadic_second_order_logic]
-
-Aliases: MSO2
-
-See also: [MSO1]
diff --git a/provenance_reasoning b/provenance_reasoning
@@ -2,6 +2,6 @@
With [description_logics]:
- [ceylan2022explanations]
-- [bourgaux2023semiring]
+- [bourgaux2023semiring] and [bourgaux2026semiring]
Up: [provenance] for [reasoning]
diff --git a/shuffle b/shuffle
@@ -7,6 +7,8 @@ A [word] w is a *shuffle* of two [words] u and v if we can interleave the charac
- a finite set of [words] can be decomposed into at most one multiset of which it is the shuffle:
- see [berstel2002shuffle]
+[shuffle] of [CFGs], cf [barloy2026shuffles]
+
Up: [formal_language_operator]
Aliases: interleaving
diff --git a/structuredness b/structuredness
@@ -4,6 +4,9 @@ A [Boolean_circuit] in [DNNF] that has a [vtree]
- [circuit_restructuring]
+[Circuit_classes]:
+- [dSDNNFs]
+
Up: [circuit_condition]
Aliases: structured circuit, structured, structured circuits, circuit structuredness