wiki_research

commit cf818e2b20cc7577655eeeb7cfddab8d6764b957
parent c61667b82897f81b10278e480e56b17b0540a27a
Author: Antoine Amarilli <a3nm@a3nm.net>
Date:   Tue, 29 Jul 2025 15:41:27 +0200

commit with codex

Diffstat:
context_free_grammar_equivalence
 | 
2
+-
context_free_grammar_finite
 | 
4
++--
dsdnnf
 | 
2
+-
first_order_model_checking
 | 
7
++++---
language_equivalence
 | 
2
+-
mengel2025lower
 | 
7
+++++++
obdd
 | 
3
++-
unambiguous_finite_cfg
 | 
7
+++++++

8 files changed, 25 insertions(+), 9 deletions(-)
diff --git a/context_free_grammar_equivalence b/context_free_grammar_equivalence
@@ -6,4 +6,4 @@ Two [CFGs] are *equivalent* if they recognize the same [formal_language]
 
 Up: [context_free_grammar], [language_equivalence]
 
-Aliases: CFG equivalence, CFG equivalent
+Aliases: CFG equivalence, CFG equivalent, equivalent CFG, grammar equivalent
diff --git a/context_free_grammar_finite b/context_free_grammar_finite
@@ -2,10 +2,10 @@
 
 A *finite CFG* is a [context_free_grammar] which represents a [finite_language]
 
-Unlike general [CFGs], for finite CFGs, there always exists a [grammar_equivalent] [unambiguous_CFG]
+Unlike general [CFGs], for finite CFGs, there always exists a [grammar_equivalent] [unambiguous_finite_CFG], but doubly exponential blowup ([mengel2025lower])
 
 Up: [context_free_grammar], [language_finite]
 
 See also: [slp], [factorized_database]
 
-Aliases: finite context free grammar
+Aliases: finite context free grammar, finite context free grammars, finite CFG, finite CFGs
diff --git a/dsdnnf b/dsdnnf
@@ -6,4 +6,4 @@ not closed under [complementation], cf [vinallsmeeth2024structured] by [harry]
 
 Up: [knowledge_compilation_classes], [ddnnf], [sdnnf]
 
-Aliases: dSDNNFs
+Aliases: dSDNNFs, d_SDNNFs, d_SDNNF
diff --git a/first_order_model_checking b/first_order_model_checking
@@ -9,14 +9,15 @@
 [first_order_property_conjecture] on the hardness of FO model checking, cf [gao2018completeness]
   - it is a weaker version of [strong_exponential_time_hypothesis]
 
-## Bounded variables
+## On specific [logical_fragments]
 
 - [first_order_model_checking_fok]
 - [first_order_model_checking_fo2]
 
-## [parameterized_complexity]
+## [Computational_complexity]
 
-[fo_model_checking_parameterized_complexity]
+[FO_model_checking_complexity]
+- [fo_model_checking_parameterized_complexity]
 
 Up: [model_checking] for [first_order_logic]
 
diff --git a/language_equivalence b/language_equivalence
@@ -10,6 +10,6 @@ test if two languages are the same
 
 Up: [formal_language_computational_problem], [equivalence]
 
-See also: [query_equivalence], [language_inclusion], [regular_expression_equivalence], [automaton_equivalence]
+See also: [query_equivalence], [language_inclusion], [regular_expression_equivalence], [automaton_equivalence], [CFG_equivalent]
 
 Aliases: language equivalent, language equivalence problem
diff --git a/mengel2025lower b/mengel2025lower
@@ -0,0 +1,7 @@
+# mengel2025lower
+
+by [stefan_mengel] and [harry], at [PODS_2025]
+
+Up: [academic_paper]
+
+Aliases: mengel2024lower
diff --git a/obdd b/obdd
@@ -5,7 +5,8 @@ A [deterministic] [bdd] with a [variable_order]
 - [uobdd]
 - [nobdd]
 
-[synthesis]: we can take [conjunction] and [disjunction] of two OBDDs where the [variable_order] is the same
+We can tractably take the [conjunction] and [disjunction] of two OBDDs where the [variable_order] is the same
+- [OBDD_conjunction]
 
 Up: [bdd]
 
diff --git a/unambiguous_finite_cfg b/unambiguous_finite_cfg
@@ -0,0 +1,7 @@
+# Unambiguous finite CFG
+
+A [finite_CFG] which is an [unambiguous_CFG]
+
+Doubly exponential separation bounds in [mengel2025lower]
+
+Up: [context_free_grammar_finite], [unambiguous_CFG]