lo.logic

  1. infinite propositional logic - compactness

  2. Automated proving that a program doesn't halt
  3. problem extracting correct results using relational algebra
  4. Extended Church-Turing Thesis
  5. Solid applications of category theory in TCS?

  6. Family of formulas for which Gabbay's separation algorithm explodes nonelementarily

  7. Is it possible to transform a theory written in FOL into an equivalent theory that uses conditional equational logic plus Boolean Algebra?
  8. Checking formulas with two quantifiers ($\forall \exists$) - 2QBF

  9. Smallest possible universal combinator

  10. Normal forms for intuitionistic formulas?
  11. FOL sentence encoding acyclic graphs using only universal quantifiers

  12. On collapsing the Exponential time hierarchy
  13. State of the Art for the Monadic Class?

  14. Algebraic account of Gaussian elimination?
  15. Conclusions from reverse mathematical strength of graph minor theorem
  16. Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

  17. What logic(s) exist for attributing belief?
  18. Expressiveness of bounded difference constraints with sets

  19. Equilibrium in a Halting Game
  20. Can we verify satisfiability of first order statements via saturation in sub-exponential time?

  21. Determine if a structure is a model of an inductively defined predicate

  22. Definitions of strongest postconditions
  23. How would I go about learning the underlying theory of the Coq proof assistant?
  24. What's the point of $\eta$-conversion in lambda calculus?

  25. Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

  26. Does the first order theory of a finite structure have bounded quantifier rank?
  27. Why does a Most General Unifier (MGU) always exist?

  28. Languages that lack contraction, weakening or exchange
  29. Question on Turings Dissertation *Systems of Logic based on Ordinals*, Axiomatic Properties
  30. What is the intuition behind linear logic?
  31. Efficiently computing the union of all minimal unsatisfiable constraint sets in a first-order unification problem

  32. Finite intersection property of polymorphic type families

  33. How to generate Skolem function in practice
  34. Relationship between Pataraia's theorem and inductive-recursive definitions?

  35. Coherence spaces and full completeness for the implicative fragment of linear logic
  36. Construct proof systems for common algorithmic task, like equivalence of regular expressions
  37. Algorithms to synthesize optimal plans satisfying temporal logic constraints
  38. Salomaa's axiomatisation of regular languages and the use of regular expression in it
  39. How to mechanically derive the recursor of a type from its constructors?

  40. Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

  41. Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

  42. Transferring results on coalgebras in one category to another
  43. Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)
  44. Is there an algorithm which gets incrementally "smarter" as it runs?
  45. Law of excluded middle in MLTT

  46. Categorical semantics for S5 modal logic?
  47. Intuitionistic fragments of classical logic

  48. About the origin of the names "immune" and "simple"
  49. Decidability of the monadic second-order theory of a class of finite structures

  50. What is First-Order Rewritable (and FO-Query)?

  51. Applications of the monoidal closed structure in LTL?

  52. Writing universal recursive function
  53. Typo in the calculus of constructions paper?
  54. What is the background in algebraic geometry and representation theory needed for geometric complexity theory?

  55. Is there a signature of a first-order language that characterize the class of regular languages?

  56. Formal definition of Turing Completeness

  57. Sequent calculus for nonmonotonic/defeasible logics?
  58. Complexity of validity of first-order logic over finite words with bounded quantifier alternation?
  59. Courcelle's theorem for bounded clique-width graphs

  60. Connection between nonmonotonic logic and type theory (lambda calculus)

  61. Evaluating boolean formula without knowing all values

  62. Can you explain an intuition behind Coherent Spaces?

  63. Forms of types in the calculus of constructions

  64. Boundary between decidability and undecidability for small theories

  65. Incomplete basis of combinators
  66. Damas-Milner-like subset of the calculus of constructions with global type inference

  67. Finding a finite model

  68. Definition for MSO2 for arbitrary structures

  69. Consistency of MSOL over trees
  70. MLTT vs. [weak] MSOL
  71. Standard reference for basic model theory definitions

  72. Correspondence between complexity classes and logic

  73. How many tautologies are there?

  74. Is there a good notion of non-termination and halting proofs in type theory?

  75. What is the difference between unification and anti-unification?

  76. In regards to the tautologies of a polynomially-bounded propositional proof system

  77. How to model degree variable in logic (new type of modal logic?)?

  78. What is the role of predicativity in inductive definitions in type theory?
  79. On the difference between propositional proof system and polynomially-bounded proof system

  80. How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses
  81. Is `sort` typeable on elementary affine logic?
  82. Minor closed properties that are explicitly MSO expressible

  83. The evaluation problem for AC$^0_d$ formulas is in FO
  84. What are natural examples of non-relativizable proofs?
  85. Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

  86. Reference for CTL* logic
  87. Are there any propositional proof systems which are not Cook-Reckhow proof systems?

  88. What is the significance of nominal techniques?

  89. Abduction in a Herbrand Constraint System

  90. Explaining Applicative functor in categorical terms - monoidal functors

  91. Logical Reations for an Impredicative System in a Predicative MetaTheory
  92. Problem in embedding

  93. Sum-of-squares proof system

  94. Is Logic Done on Superpositional Bit Values Useful?

  95. Concatenative binary lambda calculus/combinatory logic

  96. Universal and existential types
  97. Presburger Arithmetic Decision Procedures

  98. Looking for papers and articles on modal substructural logics
  99. An example where smallest normal lambda term is not fastest

  100. What's wrong with this LEAN proof?