Silvio Ghilardi

155 papers A* 5A 14B 16Journal 83Unranked 32

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A calculus for modal compact Hausdorff spaces. J. Log. Comput. Nick Bezhanishvili, Luca Carai, Silvio Ghilardi, Zhiguang Zhao
2025	J	`jnl`	First-Order Modal Logic via Logical Categories. CoRR Silvio Ghilardi, Jérémie Marquès
2024	—	`conf`	Model Completeness for Rational Trees. IJCAR (1) Silvio Ghilardi, Lia M. Poidomani
2024	J	`jnl`	Profiniteness, monadicity and universal models in modal logic. Ann. Pure Appl. Log. Matteo De Berardinis, Silvio Ghilardi
2024	B	`conf`	Unification With Simple Variable Restrictions and Admissibility of Π2-Rules. AiML Rodrigo Nicolau Almeida, Silvio Ghilardi
2024	J	`jnl`	Unification with Simple Variable Restrictions and Admissibility of Π CoRR Rodrigo Nicolau Almeida, Silvio Ghilardi
2023	J	`jnl`	Admissibility of Π Ann. Pure Appl. Log. Nick Bezhanishvili, Luca Carai, Silvio Ghilardi, Lucia Landi
2023	J	`jnl`	Interpolation Results for Arrays with Length and MaxDiff. ACM Trans. Comput. Log. Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, Chiara Naso
2023	A*	`conf`	Safety Verification and Universal Invariants for Relational Action Bases. IJCAI Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2022	J	`jnl`	A Formal Verification of ArpON - A Tool for Avoiding Man-in-the-Middle Attacks in Ethernet Networks. IEEE Trans. Dependable Secur. Comput. Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani
2022	J	`jnl`	Combination of Uniform Interpolants via Beth Definability. J. Autom. Reason. Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2022	J	`jnl`	General Interpolation and Strong Amalgamation for Contiguous Arrays. CoRR Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, Chiara Naso
2022	J	`jnl`	Petri net-based object-centric processes with read-only data. Inf. Syst. Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2022	J	`jnl`	Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version). CoRR Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2022	J	`jnl`	Uniform Interpolants in EUF: Algorithms using DAG-representations. Log. Methods Comput. Sci. Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
2021	—	`conf`	AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff. SMT José Abel Castellanos Joo, Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
2021	A	`conf`	Delta-BPMN: A Concrete Language and Verifier for Data-Aware BPMN. BPM Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2021	J	`jnl`	Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems. J. Autom. Reason. Silvio Ghilardi, Elena Pagani
2021	B	`conf`	Interpolation and Amalgamation for Arrays with MaxDiff. FoSSaCS Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
2021	J	`jnl`	Model Completeness, Uniform Interpolants and Superposition Calculus. J. Autom. Reason. Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2020	—	`conf`	Combined Covers and Beth Definability. IJCAR (1) Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2020	J	`jnl`	Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS. CoRR Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
2020	—	`conf`	Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations. CILC Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
2020	J	`jnl`	Fixed-point Elimination in the Intuitionistic Propositional Calculus. ACM Trans. Comput. Log. Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
2020	J	`jnl`	Free Heyting algebra endomorphisms: Ruitenburg's Theorem and beyond. Math. Struct. Comput. Sci. Silvio Ghilardi, Luigi Santocanale
2020	J	`jnl`	Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version). CoRR Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
2020	B	`conf`	Model Completeness and Π AiML Nick Bezhanishvili, Silvio Ghilardi, Lucia Landi
2020	A	`conf`	Petri Nets with Parameterised Data - Modelling and Verification. BPM Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2020	J	`jnl`	Petri Nets with Parameterised Data: Modelling and Verification (Extended Version). CoRR Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2020	J	`jnl`	SMT-based verification of data-aware processes: a model-theoretic approach. Math. Struct. Comput. Sci. Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	J	`jnl`	Combined Covers and Beth Definability. CoRR Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	J	`jnl`	Existentially closed Brouwerian Semilattices. J. Symb. Log. Luca Carai, Silvio Ghilardi
2019	J	`jnl`	Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version). CoRR Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	A	`conf`	Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN. BPM Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	J	`jnl`	Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN. CoRR Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	J	`jnl`	Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond. CoRR Silvio Ghilardi, Luigi Santocanale
2019	—	`conf`	From Model Completeness to Verification of Data Aware Processes. Description Logic, Theory Combination, and All That Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	—	`conf`	Model Completeness, Covers and Superposition (Abridged Version). CILC Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2019	A	`conf`	Model Completeness, Covers and Superposition. CADE Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2018	J	`jnl`	Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version). CoRR Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
2018	J	`jnl`	Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Log. Silvio Ghilardi, Alessandro Gianola
2018	J	`jnl`	Quantifier Elimination for Database Driven Verification. CoRR Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2018	B	`conf`	Ruitenburg's Theorem via Duality and Bounded Bisimulations. Advances in Modal Logic Silvio Ghilardi, Luigi Santocanale
2018	J	`jnl`	Ruitenburg's Theorem via Duality and Bounded Bisimulations. CoRR Luigi Santocanale, Silvio Ghilardi
2018	J	`jnl`	Verification of Data-Aware Processes via Array-Based Systems (Extended Version). CoRR Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
2017	J	`jnl`	A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Informaticae Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2017	J	`jnl`	A Model-Theoretic characterization of Monadic second order Logic on Infinite Words. J. Symb. Log. Silvio Ghilardi, Samuel J. van Gool
2017	J	`jnl`	Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. Francesco Alberti, Silvio Ghilardi, Elena Pagani
2017	—	`conf`	Counter Simulations via Higher Order Quantifier Elimination: a preliminary report. PxTP Silvio Ghilardi, Elena Pagani
2017	B	`conf`	Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -. IFM Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani
2017	—	`conf`	Formal verification of data-intensive applications through model checking modulo theories. SPIN Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu, Silvio Ghilardi
2017	—	`conf`	Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case). FroCoS Silvio Ghilardi, Alessandro Gianola
2017	J	`jnl`	One-step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property. J. Log. Comput. Nick Bezhanishvili, Silvio Ghilardi, Frederik Möllerström Lauridsen
2017	—	`conf`	Second Order Quantifier Elimination: Towards Verification Applications. SOQE Silvio Ghilardi, Elena Pagani
2016	J	`jnl`	Admissible Bases Via Stable Canonical Rules. Stud Logica Nick Bezhanishvili, David Gabelaia, Silvio Ghilardi, Mamuka Jibladze
2016	—	`conf`	Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies. CILC Francesco Alberti, Silvio Ghilardi, Andrea Orsini, Elena Pagani
2016	A	`conf`	Counting Constraints in Flat Array Fragments. IJCAR Francesco Alberti, Silvio Ghilardi, Elena Pagani
2016	J	`jnl`	Counting Constraints in Flat Array Fragments. CoRR Francesco Alberti, Silvio Ghilardi, Elena Pagani
2016	B	`conf`	Fixed-Point Elimination in the Intuitionistic Propositional Calculus. FoSSaCS Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
2016	J	`jnl`	Fixed-point elimination in the intuitionistic propositional calculus. CoRR Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
2016	A*	`conf`	Monadic second order logic as the model companion of temporal logic. LICS Silvio Ghilardi, Sam van Gool
2016	J	`jnl`	Monadic second order logic as the model companion of temporal logic. CoRR Silvio Ghilardi, Samuel J. van Gool
2016	—	`ed.`	Proceedings of the 30th International Workshop on Unification, UNIF 2016, Porto, Portugal, June 26, 2016. UNIF Silvio Ghilardi, Manfred Schmidt-Schauß
2015	—	`conf`	A New Acceleration-Based Combination Framework for Array Properties. FroCos Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2015	J	`jnl`	A model-theoretic characterization of monadic second order logic on infinite words. CoRR Silvio Ghilardi, Samuel J. van Gool
2015	J	`jnl`	Decision Procedures for Flat Array Properties. J. Autom. Reason. Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	—	`conf`	A Framework for the Verification of Parameterized Infinite-State Systems. CILC Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	J	`jnl`	An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2014	B	`conf`	Booster: An Acceleration-Based Verification Framework for Array Programs. ATVA Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	—	`conf`	Decision Procedures for Flat Array Properties. SMT Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	A	`conf`	Decision Procedures for Flat Array Properties. TACAS Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	—	`conf`	Monotonic Abstraction Techniques: from Parametric to Software Model Checking. MOD* Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	B	`conf`	Multiple-conclusion Rules, Hypersequents Syntax and Step Frames. Advances in Modal Logic Nick Bezhanishvili, Silvio Ghilardi
2014	J	`jnl`	Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2014	J	`jnl`	The bounded proof property via step algebras and step frames. Ann. Pure Appl. Log. Nick Bezhanishvili, Silvio Ghilardi
2014	J	`jnl`	The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination. Log. J. IGPL Silvio Ghilardi, Grigori Mints
2014	—	`ch.`	Unified Correspondence. Johan van Benthem on Logic and Information Dynamics Willem Conradie, Silvio Ghilardi, Alessandra Palmigiano
2013	J	`jnl`	Abstraction and Acceleration in SMT-based Model-Checking for Array Programs CoRR Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2013	—	`conf`	Acceleration-based safety decision procedure for programs with arrays. LPAR (short papers) Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2013	J	`jnl`	Automated Termination in Model-Checking Modulo Theories. Int. J. Found. Comput. Sci. Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
2013	B	`conf`	Bounded Proofs and Step Frames. TABLEAUX Nick Bezhanishvili, Silvio Ghilardi
2013	—	`conf`	Definability of Accelerated Relations in a Theory of Arrays and Its Applications. FroCos Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2013	—	`conf`	From free algebras to proof bounds. TACL Silvio Ghilardi
2012	B	`ed.`	Advances in Modal Logic 9, papers from the ninth conference on "Advances in Modal Logic," held in Copenhagen, Denmark, 22-25 August 2012 Advances in Modal Logic Thomas Bolander, Torben Braüner, Silvio Ghilardi, Lawrence S. Moss
2012	—	`conf`	Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
2012	J	`jnl`	From Strong Amalgamability to Modularity of Quantifier-Free Interpolation CoRR Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2012	A	`conf`	From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. IJCAR Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2012	J	`jnl`	LTL over description logic axioms. ACM Trans. Comput. Log. Franz Baader, Silvio Ghilardi, Carsten Lutz
2012	B	`conf`	Lazy Abstraction with Interpolants for Arrays. LPAR Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012	J	`jnl`	Quantifier-Free Interpolation of a Theory of Arrays Log. Methods Comput. Sci. Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2012	—	`conf`	Reachability Modulo Theory Library. SMT@IJCAR Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012	A*	`conf`	SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012	J	`jnl`	Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories. J. Satisf. Boolean Model. Comput. Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi
2011	—	`conf`	A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. FroCoS Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2011	J	`jnl`	An Algebraic Approach to Subframe Logics. Modal Case. Notre Dame J. Formal Log. Guram Bezhanishvili, Silvio Ghilardi, Mamuka Jibladze
2011	—	`conf`	Automated Termination in Model Checking Modulo Theories. RP Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
2011	—	`conf`	Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2011	J	`jnl`	Unification in modal and description logics. Log. J. IGPL Franz Baader, Silvio Ghilardi
2010	J	`jnl`	Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi
2010	J	`jnl`	Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis Log. Methods Comput. Sci. Silvio Ghilardi, Silvio Ranise
2010	J	`jnl`	Book Reviews. Stud Logica Silvio Ghilardi
2010	A	`conf`	Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study. DISC Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi
2010	J	`jnl`	Continuity, freeness, and filtrations. J. Appl. Non Class. Logics Silvio Ghilardi
2010	—	`conf`	MCMT in the Land of Parametrized Timed Automata. VERIFY@IJCAR Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
2010	A	`conf`	MCMT: A Model Checker Modulo Theories. IJCAR Silvio Ghilardi, Silvio Ranise
2010	J	`jnl`	Special issue on automated deduction: Decidability, complexity, tractability. J. Symb. Comput. Silvio Ghilardi, Viorica Sofronie-Stokkermans, Ulrike Sattler, Ashish Tiwari
2009	—	`ed.`	Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings FroCoS Silvio Ghilardi, Roberto Sebastiani
2009	B	`conf`	Goal-Directed Invariant Synthesis for Model Checking Modulo Theories. TABLEAUX Silvio Ghilardi, Silvio Ranise
2009	—	`conf`	Model-Checking of Array-Based Systems: from Foundations to Implementation. FTP Silvio Ghilardi
2008	J	`jnl`	A comprehensive combination framework. ACM Trans. Comput. Log. Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli
2008	—	`conf`	LTL over Description Logic Axioms. Description Logics Franz Baader, Silvio Ghilardi, Carsten Lutz
2008	A*	`conf`	LTL over Description Logic Axioms. KR Franz Baader, Silvio Ghilardi, Carsten Lutz
2008	—	`conf`	Light-Weight SMT-based Model Checking. AVoCS Silvio Ghilardi, Silvio Ranise, Thomas Valsecchi
2008	A	`conf`	Towards SMT Model Checking of Array-Based Systems. IJCAR Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2007	J	`jnl`	An algebraic approach to subframe logics. Intuitionistic case. Ann. Pure Appl. Log. Guram Bezhanishvili, Silvio Ghilardi
2007	A	`conf`	Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. CADE Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2007	J	`jnl`	Connecting many-sorted theories. J. Symb. Log. Franz Baader, Silvio Ghilardi
2007	J	`jnl`	Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2007	—	`ch.`	First-order modal logic. Handbook of Modal Logic Torben Braüner, Silvio Ghilardi
2007	—	`conf`	From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems. Deduction and Decision Procedures Silvio Ghilardi, Silvio Ranise, Enrica Nicolini, Daniele Zucchelli
2007	—	`conf`	Noetherianity and Combination Problems. FroCoS Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2006	J	`jnl`	A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Inf. Comput. Franz Baader, Silvio Ghilardi, Cesare Tinelli
2006	B	`conf`	Conservative extensions in modal logic. Advances in Modal Logic Silvio Ghilardi, Carsten Lutz, Frank Wolter, Michael Zakharyaschev
2006	A	`conf`	Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. IJCAR Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2006	B	`conf`	Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. JELIA Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
2006	A*	`conf`	Did I Damage My Ontology? A Case for Conservative Extensions in Description Logics. KR Silvio Ghilardi, Carsten Lutz, Frank Wolter
2005	—	`conf`	A Comprehensive Framework for Combined Decision Procedures. FroCoS Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli
2005	—	`conf`	Connecting Many-Sorted Structures and Theories Through Adjoint Functions. FroCoS Franz Baader, Silvio Ghilardi
2005	A	`conf`	Connecting Many-Sorted Theories. CADE Franz Baader, Silvio Ghilardi
2004	A	`conf`	A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. IJCAR Franz Baader, Silvio Ghilardi, Cesare Tinelli
2004	J	`jnl`	Filtering unification and most general unifiers in modal logic. J. Symb. Log. Silvio Ghilardi, Lorenzo Sacchetti
2004	J	`jnl`	Model-Theoretic Methods in Combined Constraint Satisfiability. J. Autom. Reason. Silvio Ghilardi
2004	J	`jnl`	Unification, finite duality and projectivity in varieties of Heyting algebras. Ann. Pure Appl. Log. Silvio Ghilardi
2003	B	`conf`	Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics. LPAR Silvio Ghilardi, Luigi Santocanale
2003	J	`jnl`	Combining word problems through rewriting in categories with products. Theor. Comput. Sci. Camillo Fiorentini, Silvio Ghilardi
2003	J	`jnl`	Foreword. Stud Logica Silvio Ghilardi, Daniele Mundici
2003	—	`conf`	Quantifier Elimination and Provers Integration. FTP Silvio Ghilardi
2002	J	`jnl`	A Resolution/Tableaux Algorithm for Projective Approximations in IPC. Log. J. IGPL Silvio Ghilardi
2002	—	`book`	Sheaves, games, and model completions - a categorical approach to nonclassical propositional logics. Silvio Ghilardi, Marek W. Zawadowski
2000	J	`jnl`	Best Solving Modal Equations. Ann. Pure Appl. Log. Silvio Ghilardi
2000	B	`conf`	From Bisimulation Quantifiers to Classifying Toposes. Advances in Modal Logic Silvio Ghilardi, Marek W. Zawadowski
1999	J	`jnl`	On Canonicity and Strong Completeness Conditions in Intermediate Propositional Logics. Stud Logica Silvio Ghilardi, Pierangelo Miglioli
1999	J	`jnl`	Unification in Intuitionistic Logic. J. Symb. Log. Silvio Ghilardi
1997	J	`jnl`	Constructive Canonicity in Non-Classical Logics. Ann. Pure Appl. Log. Silvio Ghilardi, Giancarlo Meloni
1997	J	`jnl`	Model Completions, r-Heyting Categories. Ann. Pure Appl. Log. Silvio Ghilardi, Marek W. Zawadowski
1997	J	`jnl`	Unification Through Projectivity. J. Log. Comput. Silvio Ghilardi
1996	J	`jnl`	Relational and Partial Variable Sets and Basic Predicate Logic. J. Symb. Log. Silvio Ghilardi, Giancarlo Meloni
1995	J	`jnl`	A Sheaf Representation and Duality for Finitely Presenting Heyting Algebras. J. Symb. Log. Silvio Ghilardi, Marek W. Zawadowski
1995	J	`jnl`	An Algebraic Theory of Normal Forms. Ann. Pure Appl. Log. Silvio Ghilardi
1995	J	`jnl`	Undefinability of propositional quantifiers in the modal system S4. Stud Logica Silvio Ghilardi, Marek W. Zawadowski
1992	J	`jnl`	Quantified Extensions of Canonical Propositional Intermediate Logics. Stud Logica Silvio Ghilardi
1991	J	`jnl`	Incompleteness Results in Kripke Semantics. J. Symb. Log. Silvio Ghilardi
1990	J	`jnl`	Modal logics with Math. Log. Q. Silvio Ghilardi, Giancarlo Meloni
1989	J	`jnl`	Directed frames. Arch. Math. Log. Giovanna Corsi, Silvio Ghilardi
1989	J	`jnl`	Presheaf semantics and independence results for some non-classical first-order logics. Arch. Math. Log. Silvio Ghilardi