... Complementando com os resumos de Favio Miranda Perea e Lourdes Huesca,
da UNAM:
Favio Ezequiel Miranda Perea (UNAM FCiencias (M\'exico))
Title of the talk: A global Curry-Howard correspondence for strong
normalization in intuitionistic logic.
Abstract of the talk: Normalization theorems are pillars of Proof Theory,
since they ensure that any derivation, usually in Natural Deduction, can be
transformed in a specific proof having no detours, and in the case of
strong normalization this can be done by simplifying redundancies in an
arbitrary way. We can classify normalization proofs as diagrammatical or
algebraic, the former are those native of the Gentzen-Prawitz tradition
where the argumentations depend on the manipulation of proof-tree diagrams,
whereas the latter are based on lambda calculi where discussions are purely
algebraic, justified by the well-known Curry-Howard correspondence.
However, both approaches are separated by an explanatory gap which
prohibits the interpretation of lambda terms by proof trees in a non-local
manner. That is, beyond the mapping of a lambda term into a particular
instance of an inference rule. In this talk we propose an algebraic proof
representation by means of enhanced lambda terms that capture not only the
proof search process of a detour but also provide an encoding of global
proof trees including ellipsis, which are common in structural proof theory
arguments. This way we provide a lambda calculus which conciliates both
approaches in the case of intuitionistic logic, allowing to construct a
mechanizable strong normalization proof that keeps the proof-theoretical
intuition, thus providing not only guarantee but explanation. This research
is being supported by UNAM-DGAPA-PAPIIT grant IN101723.
Lourdes del Carmen Gonz\'alez Huesca (UNAM FCiencias (M\'exico))
Title of the talk: On multiary rules
Abstract of the talk: In proof-assistants, there are proof methodologies
that are non directly referred to deductive systems. There is a gap between
a formal system or logic, for instance, the Calculus of Inductive
Constructions, and the practical side of it.
In this talk, we analyse the useful \texttt{apply} tactic in the Rocq
proof-assistant. The internal mechanism of Rocq does not show a transparent
application of the tactic, while in a deductive system can be seen as an
iterated application of left-rules for the operators `forall' and
`implication'. The proposal of a multiary rule corresponding to the
\texttt{apply} tactic gives a family of rule-schemas showing the low-level
requirements of such tactic.
Em quarta-feira, 27 de agosto de 2025 às 12:14:20 UTC-3, samuel escreveu:
> Prezados,
>
> Seguindo com a tradição de manter sessões especiais de Lógica Matemática
> nos encontros bilaterais entre a Sociedade Brasileira de Matemática e suas
> homólogas de outros países nos últimos anos (Brasil-Espanha 2015,
> Brasil-Italia 2016, Brasil-França 2019 e Brasil-Portugal 2022, não
> esquecendo da palestra da Profa. Itala D'Ottaviano no Brasil-Estados Unidos
> de 2008), sempre com o apoio da Sociedade Brasileira de Lógica,
>
> Segue a programação da Sessão Especial de Lógica Matemática no 1st Joint
> Meeting Brazil México in Mathematics, evento esse que vai ocorrer entre os
> dias 08 e 12 de Setembro em Fortaleza, Ceará, no Hotel Mareiro.
>
> A Sessão Especial de Lógica Matemática vai ocorrer nas tardes da segunda e
> da terça-feira, dias 08 e 09 de Setembro.
>
> Programação:
>
> Lunes, 08 Septiembre
>
> 14h-14h30 Claudia Nalon (UnB)
> 14h30-15h Nancy Nunez (UNAM)
> 15h-15h30 Francisco Hernandez Quiroz (UNAM)
>
> 15h30-16h30 Coffee Break
>
> 16h30-17h Favio Miranda Perea (UNAM)
> 17h-17h30 Daniel Ventura (UFG)
> 17h30-18h Lourdes Gonzales Huesca (UNAM)
>
> Martes, 09 Septiembre
>
> 14h-14h30 Ulises Ariet Ramos Garcia (UNAM Morelia)
> 14h30-15h Samuel Gomes da Silva / Ciro Russo (UFBA)
> 15h-15h30 Salvador Garcia-Ferreira (UNAM Morelia)
>
> 15h30-16h30 Coffee break
>
> Resumos:
>
>
> ***************************************************************************************
>
> Claudia Nalon (UnB (Brazil))
> Title of the talk: Automated Reasoning for Non-Classical Logics
> Abstract of the talk: We will discuss two different
> resolution-based calculi for the multimodal logic Kn with particular focus
> on the characteristics that have impact on theorem-proving. We will report
> on experimental results and the influence of proof strategies and
> processing techniques for both calculi.
>
> Francisco Hern\'andez Quiroz (UNAM FCiencias (México))
> Title of the talk: Inferential Information Complexity
> Abstract of the talk: An analogous to Kolmogorov complexity can be
> used to measure the epistemic contribution of deduction. Minimal proof
> length (in terms of inferential steps) in decidable systems is a good
> indication of the minimal information needed to prove a theorem. This
> measure is independent of the chosen proof system, provided it meets some
> natural requirements.
>
> Salvador Garcia-Ferreira (UNAM (Morelia, México))
> Title of the talk: Semigroup actions and filters
> Abstract of the talk: We will show the importance of certain
> filters on a semigroup when it acts on a compact metric space. Mainly, in
> the study of the invariant closed subsets. We give several examples of such
> filters in various semigroups. We present also examples of actions of
> semigroups on countable compact metric spaces.
>
> Samuel Gomes da Silva (UFBA (Brazil))
> Title of the talk: On Forcing Axioms and Weakenings of the Axiom
> of Choice\\
> Abstract of the talk: We prove forcing axiom equivalents of two
> families of weakenings of the Axiom of Choice (like the hundreds listed in
> the standard reference Howard and Rubin, ``Consequences of the Axiom of
> Choice''):
> a trichotomy principle for cardinals isolated by L\'evy,
> $H_\kappa$, and $DC_\kappa$, the principle of dependent choices generalized
> to cardinals $\kappa$, for regular cardinals $\kappa$. Using these
> equivalents we obtain new forcing axiom formulations of the Axiom of
> Choice, $\mathbf{AC}$. A point of interest is that we use a new template
> for forcing axioms. For the class of forcings to which we asks that the
> axioms apply, we do not ask that they apply to all collections of dense
> sets of a certain cardinality (as previously done by Viale and others), but
> rather only for each particular forcing to a specific family of dense sets
> of the cardinality in question.
>
> Ciro Russo (UFBA (Brazil))
> Title of the talk: Priestley-type Duality for positive MV-algebras \\
> Abstract of the talk: In this talk we shall present a Priestley-type
> duality between positive MV algebras and a suitable class of ordered fuzzy
> topological spaces. The duality theorem will include, as special cases,
> both the classical Priestley duality and the Stone-type duality proved by
> the speaker in a previous work.
>
>
> Ulises Ariet Ramos-Garcia (UNAM MatMorelia (México))
> Title of the talk: Hindman-tall ideals and the Ramsey property for
> pairs in ordered-union ultrafilters
> Abstract of the talk: We will show an equivalence between the
> Ramsey's property for pairs in ordered-union ultrafilters on FIN in terms
> of Hindman-tall ideals on FIN. This characterization is useful to address
> an old problem of A. Blass asking if every ordered-union ultrafilter has
> the Ramsey's property for pairs. This work is in collaboration with Angel
> Augusto Camacho-Acosta and Carlos L\'opez-Callejas.
>
> Daniel Ventura (UFG (Brazil))
> Title of the talk: Linearisation Based on Normalisation
> Strategies\\
> Abstract of the talk: Linear terms/functions have interesting
> properties, such as no infinite reductions, typability in polynomial time,
> and simpler and optimised abstract machines for their execution, due to
> their no-duplication operational semantics. Linearisation of
> strong-normalising terms has been proposed based on typing information an
> intersection types system provides. More recently, a weak-linearisation
> procedure --originally defined through a static characterisation of virtual
> redices, based on legal paths computed from the term syntactic tree--, was
> devised based on a quantitative type system. In such a procedure, functions
> not applied in any reduction path are not linearised. Therefore, the
> quantitative system provides information related to a maximal normalisation
> strategy. In this work, we explore linearisation procedures based on
> different normalisation strategies.
>
> Favio Ezequiel Miranda Perea (UNAM (México))
> Title of the talk: TBA
> Abstract of the talk: TBA
>
> Lourdes del Carmen Gonzalez Huesca (UNAM (México))
> Title of the talk: TBA
> Abstract of the talk: TBA
>
> Nancy Abigail Nunez Hernandez (UNAM-FES, Acatlan (México))
> Title of the talk: Why AI is not going to take mathematicians'
> jobs (or on the complexity of mathematicians' jobs)
> Abstract of the talk: The rapid development of AI is causing a lot
> of concern among many people working in a wide variety of fields: teachers,
> journalists, lawyers, physicians, and even programmers are worried about
> losing their jobs to some form of AI. The question that I want to explore
> in this work is whether AI can also take mathematicians' jobs. In 1956,
> G\"odel wrote to von Neuman inquiring whether "the reasoning of
> mathematicians about yes-or-no questions can be completely replaced by
> machines." (Hartmanis 1993, p. 6) This letter has become famous among
> theoretical computer scientists interested in the open problem of
> determining if P and NP are different complexity classes. Although G\"odel
> was inquiring about an NP-complete problem (Buss 1995), a mathematician's
> job is also directly related to coNP-complete problems; for instance, when
> they have to decide whether a given sentence follows from some set of
> axioms or other theorems. This work proposes that because of the complexity
> of the problems mathematicians deal with, AI should not be able to take
> their jobs so easily.
>
>
> ****************************************************************************************
>
> Todos os interessados que possam comparecer, sintam-se fortemente
> convidados !
>
> Atenciosamente
>
> []s Samuel, em nome dos organizadores da Sessão (Samuel e João Marcos
> pelo Brasil, Lourdes Huesca e Favio Miranda-Perea pelo México).
>
>
>
--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica
<[email protected]>
---
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um
e-mail para [email protected].
Para ver esta conversa, acesse
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/62c43542-9190-4d54-a7ad-a215e2fb34dcn%40dimap.ufrn.br.
