Marcelo Finger

FLAP Journal 2025 Journal Article

Logic in Times of Big Data

• Marcelo Finger

Big data is all over us these days. In computational terms, logics are com- plex, at times undecidable, so how can it tackle the challenges of Big Data. In this shor piece in honor of Dov Gabbay, I discuss the weak points of employing logic, just to argue that logic should be used for what logic does best. Namely, proving properties of system, in particular the neural networks that are used to process big data application. We then discuss how Łukasiewicz Infinitely- valued Logic can be used for that purpose, and provide a brief presentation of the topic.

KER Journal 2023 Journal Article

Selecting and ranking leading cases in Brazilian Supreme Court decisions

• Jackson José De Souza
• Marcelo Finger
• Jorge Alberto A. de Araújo
• Juliano Maranhão

Abstract This work studies quantitative measures for ranking judicial decisions by the Brazilian Supreme Court [Supremo Tribunal Federal (STF)] and selecting leading cases, which are understood as those with broadness of influence on different legal fields. The measures are based on a network built over decisions whose cases were finalized in the Brazilian Supreme Court between 01/2001 and 12/2019, which were obtained by crawling publicly available STF records. Three ranking measures are proposed; two are adaptations of the PageRank algorithm, and one adapts Kleinberg’s algorithm. Such measures are compared with respect to agreement on top 100 rankings; we also analyze each robustness measure based on self-agreement under perturbation. We examine whether the resulting quantitative ranking is congenial to a qualitative intuition of what the legal community usually considers as relevant precedents. We also discuss some possible criteria of relevance in the seek for patterns that suggest how quantitative and qualitative measures would better align. The ranking of leading cases and relevant decisions improved after building decision networks without irrelevant appeals and decisions that overflow the court offers a starting point to discuss the role of STF in the Brazilian judicial system. In our last work, both versions of PageRank and Kleinberg algorithms produced different rankings and all of them were robust with respect to 10% and 20%-perturbation levels, but none of them retrieved leading cases at the top of these rankings. Then, we took a further step in the studies of the STF decision network and we introduced better filtering of network nodes guided by legal expertise on the works of the Supreme Court. We also introduced more fine-grained perturbance levels to understand the impact of such filters in the STF decision network. We concluded that after filtering low-relevance decision types, the STF decision network is still robust under 10%-perturbation, but it presents higher degradation by increasing perturbation levels. The two versions of PageRank still produce different rankings. Kleinberg’s algorithm provides a different ranking, with many relevant criminal cases. Although we improved algorithms rankings filtering decisions from the network, which represents an important methodological step, there is still room for improvement. Given that relevant decisions are well ranked after filtering out a large amount of irrelevant decisions, the results set a starting point to discuss the role of STF in the Brazilian judicial system.

NeSy Conference 2019 Conference Paper

Using neural models to perform inference

• Felipe de Souza Salvatore
• Sandro Preto
• Marcelo Finger
• Roberto Hirata Jr.

AAAI Conference 2017 Conference Paper

Algorithms for Deciding Counting Quantifiers over Unary Predicates

• Marcelo Finger
• Glauber de Bona

We study algorithms for fragments of first order logic extended with counting quantifiers, which are known to be highly complex in general. We propose a fragment over unary predicates that is NP-complete and for which there is a normal form where Counting Quantification sentences have a single Unary predicate, thus call it the CQU fragment. We provide an algebraic formulation of the CQU satisfiability problem in terms of Integer Linear Programming based on which two algorithms are proposed, a direct reduction to SAT instances and an Integer Linear Programming version extended with a column generation mechanism. The latter is shown to lead to a viable implementation and experiments shows this algorithm presents a phase transition behavior.

KR Conference 2016 Conference Paper

Consolidating Probabilistic Knowledge Bases viaBelief Contraction

• Glauber de Bona
• Marcelo Finger
• Márcio Ribeiro
• Yuri Santos
• Renata Wassermann

In this work we focus on the consolidation of condiThis paper is set to study the applicability of AGM-like operations to probabilistic bases. We focus on the problem of consistency restoration, also called consolidation or contraction by falsity. We aim to identify the reasons why the set of AGM postulates based on discrete operations of deletions and accretions is too coarse to treat finely adjustable probabilistic formulas. We propose new principles that allow one to deal with the consolidation of inconsistent probabilistic bases, presenting a finer method called liftable contraction. Furthermore, we show that existing methods for probabilistic consolidation via distance minimization are particular cases of the methods proposed.

AIJ Journal 2015 Journal Article

Measuring inconsistency in probabilistic logic: rationality postulates and Dutch book interpretation

• Glauber de Bona
• Marcelo Finger

Inconsistency measures have been proposed as a way to manage inconsistent knowledge bases in the AI community. To deal with inconsistencies in the context of conditional probabilistic logics, rationality postulates and computational efficiency have driven the formulation of inconsistency measures. Independently, investigations in formal epistemol-ogy have used the betting concept of Dutch book to measure an agent's degree of incoherence. In this paper, we show the impossibility of joint satisfiability of the proposed postulates, proposing to replace them by more suitable ones. Thus we reconcile the rationality postulates for inconsistency measures in probabilistic bases and show that several inconsistency measures suggested in the literature and computable with linear programs satisfy the reconciled postulates. Additionally, we give an interpretation for these feasible measures based on the formal epistemology concept of Dutch book, bridging the views of two so far separate communities in AI and Philosophy. In particular, we show that incoherence degrees in formal epistemology may lead to novel approaches to inconsistency measures in the AI view.

TCS Journal 2015 Journal Article

Special Issue: Selected papers of the 7th and 8th workshops on Logical and Semantic Frameworks with Applications (LSFA)

• Marcelo Finger
• Delia Kesner

TCS Journal 2013 Journal Article

Semantics and proof-theory of depth bounded Boolean logics

• Marcello D’Agostino
• Marcelo Finger
• Dov Gabbay

We present a unifying semantical and proof-theoretical framework for investigating depth-bounded approximations to Boolean Logic, namely approximations in which the number of nested applications of a single structural rule, representing the classical Principle of Bivalence, is bounded above by a fixed natural number. These approximations provide a hierarchy of tractable logical systems that indefinitely converge to classical propositional logic. The framework we present here brings to light a general approach to logical inference that is quite different from the standard Gentzen-style approaches, while preserving some of their nice proof-theoretical properties, and is common to several proof systems and algorithms, such as KE, KI and Stålmarck’s method.

SAT Conference 2013 Conference Paper

Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability

• Marcelo Finger
• Ronan LeBras
• Carla P. Gomes
• Bart Selman

Abstract Practical problems often combine real-world hard constraints with soft constraints involving preferences, uncertainties or flexible requirements. A probability distribution over the models that meet the hard constraints is an answer to such problems that is in the spirit of incorporating soft constraints. We propose a method using SAT-based reasoning, probabilistic reasoning and linear programming that computes such a distribution when soft constraints are interpreted as constraints whose violation is bound by a given probability. The method, called Optimized Probabilistic Satisfiability (oPSAT), consists of a two-phase computation of a probability distribution over the set of valuations of a SAT formula. Algorithms for both phases are presented and their complexity is discussed. We also describe an application of the oPSAT technique to the problem of combinatorial materials discovery.

IJCAI Conference 2011 Conference Paper

Probabilistic Satisfiability: Logic-Based Algorithms and Phase Transition

• Marcelo Finger
• Glauber de Bona

In this paper, we study algorithms for probabilistic satisfiability (PSAT), an NP-complete problem, and their empiric complexity distribution. We define a PSAT normal form, based on which we propose two logic-based algorithms: a reduction of normal form PSAT instances to SAT, and a linear-algebraic algorithm with a logic-based column generation strategy. We conclude that both algorithms present a phase transition behaviour and that the latter has a much better performance.

TCS Journal 2006 Journal Article

The universe of propositional approximations

• Marcelo Finger
• Renata Wassermann

The idea of approximate entailment has been proposed by Schaerf and Cadoli [Tractable reasoning via approximation, Artif. Intell. 74(2) (1995) 249–310] as a way of modelling the reasoning of an agent with limited resources. In that framework, a family of logics, parameterised by a set of propositional letters, approximates classical logic as the size of the set increases. The original proposal dealt only with formulas in clausal form, but in Finger and Wassermann [Approximate and limited reasoning: semantics, proof theory, expressivity and control, J. Logic Comput. 14(2) (2004) 179–204], one of the approximate systems was extended to deal with full propositional logic, giving the new system semantics, an axiomatisation, and a sound and complete proof method based on tableaux. In this paper, we extend another approximate system by Schaerf and Cadoli, presented in a subsequent work [M. Cadoli, M. Schaerf, The complexity of entailment in propositional multivalued logics, Ann. Math. Artif. Intell. 18(1) (1996) 29–50] and then take the idea further, presenting a more general approximation framework of which the previous ones are particular cases, and show how it can be used to formalise heuristics used in theorem proving.

JELIA Conference 2004 Conference Paper

Polynomial Approximations of Full Propositional Logic via Limited Bivalence

• Marcelo Finger

Abstract The aim of this paper is to study an anytime family of logics that approximates classical inference, in which every step in the approximation can be decided in polynomial time. For clausal logic, this task has been shown to be possible by Dalal [Dal96a, Dal96b]. However, Dalal’s approach cannot be applied to full classical logic. In this paper we provide a family of logics, called Limited Bivalence Logics, that approximates full classical logic. Our approach contains two stages. In the first stage, a family of logics parameterised by a set of formulas Σ is presented. A lattice-based semantics is given and a sound and complete tableau-based proof-theory is developed. In the second stage, the first family is used to create another approximation family, in which every approximation step is shown to be polynomially decidable.

TCS Journal 2004 Journal Article

The decidability of a fragment of BB′IW-logic

• Sabine Broda
• Luı́s Damas
• Marcelo Finger
• Paulo Silva e Silva

Despite its simple formulation, the decidability of the logic BB ′ IW has remained an open problem. We present here a decision procedure for a fragment of it, called the arity-1 formulas. The decidability proof is based on a representation of formulas called formula-trees, which is coupled with a proof method that computes long normal λ-terms that inhabit a formula. A rewriting-system is associated with such λ-terms, and we show that a formula admits a BB ′ IW -λ-term if and only if the associated rewriting-system terminates. The fact that termination is decidable is proved using a result on the finiteness of non-ascending sequences of n-tuples in N n, which is equivalent to Kripke's Lemma.

ECAI Conference 2002 Conference Paper

Expressivity and Control in Limited Reasoning

• Marcelo Finger
• Renata Wassermann

TIME Conference 1998 Conference Paper

Temporal Data Obsolescence: Modelling Problems

• Marcelo Finger
• Flávio S. Corrêa da Silva

Data and knowledge bases model certain aspects of the world. When the state of the world changes faster than our ability to discover these state changes and update the data repositories accordingly, the confidence on the validity of data decays with time, and software systems running in such environments have to cope with the decay of confidence in the data lest they run the risk of giving wrong answers and behaving erroneously. This gradual loss of confidence in stored data is termed information obsolescence, and it is inherently a temporal phenomenon. We have come across such a problem when designing an information system for traffic monitoring and control in a large city, and investigate some problems related to this modelling task. We propose two approaches to deal with information obsolescence, the analytical approach and the algebraic approach, and show how both can converge to a general, temporal treatment of obsolescence. Our immediate goal is to try to approximate and reduce the whole problem of monitoring and controlling obsolescence of information to a purely temporal phenomenon, so that we can model the system using conventional temporal database technology.

TIME Conference 1997 Conference Paper

Concurrency Control for Perceivedly Instantaneous Transactions in Valid-Time Databases

• Marcelo Finger
• Peter McBrien

Although temporal databases have received considerable attention as a topic for research, little work in the area has paid attention to the concurrency control mechanisms that might be employed in temporal databases. This paper describes how the notion of the current time-also called 'now'-in valid-time databases can cause standard serialisation theory to give what are at least unintuitive results, if not actually incorrect results. The paper then describes two modifications to standard serialisation theory which correct the behaviour to give what we term perceivably instantaneous transactions: transactions where serialising T/sub 1/ and T/sub 2/ as [T/sub 1/, T/sub 2/] always implies that the current time seen by T/sub 1/ is less than or equal to the current time seen by T/sub 2/.