commit 0b56ec4f4989dc386cae015d01cb2a59ee102a82
parent 2d3b9848dc9a9351f307887834801dfae0b17a4c
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Thu, 30 Apr 2026 12:26:23 +0200
Merge remote-tracking branch 'origin/master'
Diffstat:
13 files changed, 49 insertions(+), 4 deletions(-)
diff --git a/cut_and_paste_updates b/cut_and_paste_updates
@@ -2,5 +2,6 @@
- [split_update]
- [concatenation_update]
+- [enumeration_cut_and_paste_updates]
Up: [update_word]
diff --git a/database_dependency b/database_dependency
@@ -29,3 +29,5 @@ An [implication] in [first_order_logic] with [universal_quantifiers] and with a
Up: [integrity_constraint]
Aliases: dependencies, dependency, database dependencies
+
+See also: [reasoning_rules]
diff --git a/database_repairs b/database_repairs
@@ -13,4 +13,4 @@ Up: [database_theory]
See also: [language_repair], [graph_modification], [query_repairs], [data_cleaning]
-Aliases: database repair
+Aliases: database repair, data repair, data repairs
diff --git a/decidable_fo_fragments b/decidable_fo_fragments
@@ -8,6 +8,8 @@ cf survey [hustadt2004survey]
- [guarded_fragment], cf [guarded_fragment_satisfiability]
- [FO2], cf [FO2_satisfiability]
+Also: [decidable_fo_fragments_finite]
+
Up: [FO_fragments], [satisfiability_FO]
Aliases: decidable FO fragment
diff --git a/decidable_fo_fragments_finite b/decidable_fo_fragments_finite
@@ -0,0 +1,14 @@
+# Decidable FO fragments finite
+
+[FO_fragments] for which [satisfiability_FO_finite] is [decidable]
+
+Question here: https://cstheory.stackexchange.com/questions/57103/decidable-fragments-of-first-order-logic-over-finite-structures
+
+List:
+
+- [decidable_fo_fragments] enjoying the [finite_model_property]
+- [C2]
+- [muGF]
+- [fluted_fragment] with one [transitive_relation], cf [pratt2022fluted]
+
+Up: [decidable_fo_fragments]
diff --git a/finite_satisfiability_fo b/finite_satisfiability_fo
@@ -0,0 +1,11 @@
+# Finite satisfiability FO
+
+The [computational_problem] of deciding whether an input [FO] formula is [finitely_satisfiable]
+
+- [decidable_FO_fragments_finite]
+
+See also: [satisfiability_fo]
+
+Aliases: FO satisfiability finite, satisfiability FO finite
+
+Up: [finite_satisfiability], [FO]
diff --git a/guarded_fixpoint_logic b/guarded_fixpoint_logic
@@ -0,0 +1,7 @@
+# Guarded fixpoint logic
+
+Does not have the [finite_model_property], see [barany2012finite]
+
+Up: [guarded_fragment], [fixpoint]
+
+Aliases: muGF
diff --git a/reachability b/reachability
@@ -8,4 +8,4 @@
Up: [computational_problem], [graph_theory]
-Aliases: reachability problem
+Aliases: reachability problem, reachability problems
diff --git a/regular_language_dichotomies b/regular_language_dichotomies
@@ -9,6 +9,8 @@
- [bagan2020trichotomy] about [simple_path_trichotomy]
- [martens2023trichotomy] about [trail_trichotomy]
+- [amarilli2026out] about [out_of_order_membership]
+
Up: [regular_language], [dichotomy]
-See also: [trichotomy]
+See also: [trichotomy], [query_stratification]
diff --git a/satisfiability b/satisfiability
@@ -13,3 +13,5 @@ Tools: [sat_solver]
See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability], [enumeration_valuations], [satisfiability_finite]
Up: [computational_problem]
+
+Aliases: satisfiable
diff --git a/satisfiability_finite b/satisfiability_finite
@@ -4,7 +4,8 @@ Like [satisfiability] but deciding whether a [logic_formula] has a [finite_model
- [finite_model_property]
- [finite_controllability]
+- [finite_satisfiability_FO]
Up: [satisfiability]
-Aliases: finite satisfiability, finsat
+Aliases: finite satisfiability, finsat, finitely satisfiable
diff --git a/shortest_path b/shortest_path
@@ -15,6 +15,7 @@ Related:
Variants:
- [shortest_path_almost]
+- [algebraic_path_problem]
[shortest_path_algorithm]
diff --git a/structuredness b/structuredness
@@ -4,6 +4,8 @@ A [Boolean_circuit] in [DNNF] that has a [vtree]
- [circuit_restructuring]
+- [circuit_structuredness_detecting]
+
[Circuit_classes]:
- [dSDNNFs]
