Explore the vast range of titles available.

This volume contains the proceedings of the 20th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2025), which was held in Brasilia, the capital of Brazil, from October 7 to October 8, 2025. The aim of the LSFA series of workshops is bringing together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. LSFA includes areas such as proof and type theory, equational deduction and rewriting systems, automated reasoning and concurrency theory.

We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from Isabelle formalizations and the TPTP library.

The finite models of a universal sentence$\\Phi$in a finite relational signature are the age of a structure if and only if$\\Phi$has the joint embedding property. We prove that the computational problem whether a given universal sentence$\\Phi$has the joint embedding property is undecidable, even if$\\Phi$is additionally Horn and the signature of$\\Phi$only contains relation symbols of arity at most two.

Let$\\Bigl\\langle\\matrix{n\\cr k}\\Bigr\\rangle$ ,$\\Bigl\\langle\\matrix{B_n\\cr k}\\Bigr\\rangle$ , and$\\Bigl\\langle\\matrix{D_n\\cr k}\\Bigr\\rangle$be the Eulerian numbers in the types A, B, and D, respectively -- that is, the number of permutations of n elements with$k$descents, the number of signed permutations (of$n$elements) with$k$type B descents, the number of even signed permutations (of$n$elements) with$k$type D descents. Let$S_n(t) = \\sum_{k = 0}^{n-1} \\Bigl\\langle\\matrix{n\\cr k}\\Bigr\\rangle t^k$ ,$B_n(t) = \\sum_{k = 0}^n \\Bigl\\langle\\matrix{B_n\\cr k}\\Bigr\\rangle t^k$ , and$D_n(t) = \\sum_{k = 0}^n \\Bigl\\langle\\matrix{D_n\\cr k}\\Bigr\\rangle t^k$ . We give bijective proofs of the identity$$B_n(t^2) = (1 + t)^{n+1}S_n(t) - 2^n tS_n(t^2)$$and of Stembridge's identity$$D_n(t) = B_n(t) - n2^{n-1}tS_{n-1}(t).$$These bijective proofs rely on a representation of signed permutations as paths. Using this representation we also establish a bijective correspondence between even signed permutations and pairs$(w, E)$with$([n], E)$a threshold graph and$w$a degree ordering of$([n], E)$ , which we use to obtain bijective proofs of enumerative results for threshold graphs.

Semi-unification is the combination of first-order unification and first-order matching. The undecidability of semi-unification has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s by Turing reduction from Turing machine immortality (existence of a diverging configuration). The particular Turing reduction is intricate, uses non-computational principles, and involves various intermediate models of computation. The present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes RE-completeness of semi-unification under many-one reductions. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. Arguably, this serves as comprehensive, precise, and surveyable evidence for the result at hand. The mechanization is incorporated into the existing, well-maintained Coq library of undecidability proofs. Notably, a variant of Hooper's argument for the undecidability of Turing machine immortality is part of the mechanization.

We consider nondeterministic higher-order recursion schemes as recognizers of languages of finite words or finite trees. We propose a type system that allows to solve the simultaneous-unboundedness problem (SUP) for schemes, which asks, given a set of letters A and a scheme G, whether it is the case that for every number n the scheme accepts a word (a tree) in which every letter from A appears at least n times. Using this type system we prove that SUP is (m-1)-EXPTIME-complete for word-recognizing schemes of order m, and m-EXPTIME-complete for tree-recognizing schemes of order m. Moreover, we establish the reflection property for SUP: out of an input scheme G one can create its enhanced version that recognizes the same language but is aware of the answer to SUP.