Fabio Papacchini

Fabio Papacchini

See Latest Publications
See Most Cited Publications
SciProfiles
ORCID Profile
Google Scholar

Fabio Papacchini has a total of 37 co-authors. Here are the top co-authors by number of shared publications:

Latest Publications

  • Website
    Google Scholar
    Open Access

    Model Construction for Modal Clauses

    by Ullrich Hustadt, Fabio Papacchini, Cláudia Nalon, Clare Dixon

    We present deterministic model construction algorithms for sets of modal clauses saturated with respect to three refinements of the modal-layered resolution calculus implemented in the prover "Image missing". The model construction algorithms are inspired by the Bachmair-Ganzinger method for constructing a model for a set of ground first-order clauses saturated with respect to ordered resolution with selection. The challenge is that the inference rules of the modal-layered resolution calculus for modal operators are more restrictive than an adaptation of ordered resolution with selection for these would be. While these model construction algorithms provide an alternative means to proving completeness of the calculus, our main interest is the provision of a ‘certificate’ for satisfiable modal formulae that can be independently checked to assure a user that the result of "Image missing" is correct. This complements the existing provision of proofs for unsatisfiable modal formulae.

    Cited by 1
  • Website
    Google Scholar
    Open Access

    Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic

    by Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon

    We are interested in widening the reasoning support for propositional modal logics in the so-called modal cube. The modal cube consists of extensions of the basic modal logic $$\textsf{K}_{}$$ K with an arbitrary combination of the modal axioms $$\textsf{B}$$ B , $$\textsf{D}$$ D , $$\textsf{T}$$ T , $$\textsf{4}$$ 4 and $$\textsf{5}$$ 5 . We revisit recently developed local reductions from all logics in the modal cube to a normal form comprising sets of clausal formulae with associated modal levels. We extend these reductions further to the basic modal logic $$\textsf{K}_{}$$ K , called definitional reductions. This enables any prover for $$\textsf{K}_{}$$ K to be used to solve the satisfiability problem for all logics in the modal cube. We also present alternative, axiomatic, reductions based on ideas originally proposed by Kracht, providing new theoretical results and improved bounds on the size of the reductions. We compare both sets of reductions combined with state-of-the-art provers for $$\textsf{K}_{}$$ K on a large set of parametric benchmarks for all logics in the modal cube. The results show that the provers perform better with reductions based on the clausal normal form than the axiomatic reductions.

    Cited by 4
  • Website
    Google Scholar
    Open Access

    Correction to: Local is Best: Efficient Reductions to Modal Logic K

    by Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon

  • Website
    Google Scholar
    Open Access

    Local Reductions for the Modal Cube

    by Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon

    The modal logic $${\mathsf {K}}$$K is commonly used to represent and reason about necessity and possibility and its extensions with combinations of additional axioms are used to represent knowledge, belief, desires and intentions. Here we present local reductions of all propositional modal logics in the so-called modal cube, that is, extensions of $${\mathsf {K}}$$K with arbitrary combinations of the axioms $${\mathsf {B}}$$B , $${\mathsf {D}}$$D , $${\mathsf {T}}$$T , $${\mathsf {4}}$$4 and $${\mathsf {5}}$$5 to a normal form comprising a formula and the set of modal levels it occurs at. Using these reductions we can carry out reasoning for all these logics with the theorem prover "Image missing". We define benchmarks for these logics and experiment with the reduction approach as compared to an existing resolution calculus with specialised inference rules for the various logics.

    Cited by 7
  • Website
    Google Scholar
    Open Access

    Local is Best: Efficient Reductions to Modal Logic K

    by Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon

    We present novel reductions of extensions of the basic modal logic $${\textsf {K} }$$ K with axioms $$\textsf {B} $$ B , $$\textsf {D} $$ D , $$\textsf {T} $$ T , $$\textsf {4} $$ 4 and $$\textsf {5} $$ 5 to Separated Normal Form with Sets of Modal Levels $$\textsf {SNF} _{sml}$$ SNF sml . The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to $$\textsf {SNF} _{sml}$$ SNF sml combined with a reduction to $$\textsf {SNF} _{ml}$$ SNF ml allow us to use the local reasoning of the prover $${\text {K}_{\text {S}}}{\text {P}}$$ K S P to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover $${\text {K}_{\text {S}}}{\text {P}}$$ K S P performs well when compared with a specialised resolution calculus for these logics, the built-in reductions of the first-order prover SPASS, and the higher-order logic prover LEO-III.

    Cited by 1
  • Website
    Google Scholar

    StreamB: A Declarative Language for Automatically Processing Data Streams in Abstract Environments for Agent Platforms

    by Angelo Ferrando, Fabio Papacchini

    Cited by 1
  • Website
    Google Scholar
    Open Access

    Bridging the gap between single- and multi-model predictive runtime verification

    by Angelo Ferrando, Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Fabio Papacchini, Michael Fisher, Viviana Mascardi

    This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension Multi-Model PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a centralised or a compositional way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.

    Cited by 10
  • Website
    Google Scholar

    MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest

    by Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini, Matt Luckcuck, Sven Linker, Terry R. Payne

    Cited by 3
  • Website
    Google Scholar

    Automated Planning and BDI Agents: A Case Study

    by Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini

    Cited by 7
  • Website
    Google Scholar
    Open Access

    Efficient Local Reductions to Basic Modal Logic

    by Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon

    We present novel reductions of the propositional modal logics "Image missing" , "Image missing" , "Image missing" , "Image missing" and "Image missing" to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover "Image missing" to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover "Image missing" performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.

    Cited by 7
Show all