wiki_research

commit c4a1d201611bda5e0c0d27f7903bc09a31ecd59c
parent e8bade69562ddecb34f8417ab7fa9ad26e6a347b
Author: Antoine Amarilli <a3nm@a3nm.net>
Date:   Thu, 30 Apr 2026 10:46:05 +0200

commit with codex

Diffstat:
decidable_fo_fragments
 | 
2
++
decidable_fo_fragments_finite
 | 
14
++++++++++++++
finite_satisfiability_fo
 | 
11
+++++++++++
guarded_fixpoint_logic
 | 
7
+++++++
satisfiability
 | 
2
++
satisfiability_finite
 | 
3
++-
shortest_path
 | 
1
+

7 files changed, 39 insertions(+), 1 deletion(-)
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/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]