2023
Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models.
J. Log. Algebraic Methods Program., 2023
Tableaux for Realizability of Safety Specifications.
Proceedings of the Formal Methods - 25th International Symposium, 2023
2022
A Tableau Method for the Realizability and Synthesis of Reactive Safety Specifications.
CoRR, 2022
2021
Verified Model Checking for Conjunctive Positive Logic.
SN Comput. Sci., 2021
2020
Branching-time logic ECTL# and its tree-style one-pass tableau: Extending fairness expressibility of ECTL+.
Theor. Comput. Sci., 2020
One-Pass Context-Based Tableaux Systems for CTL and ECTL.
Proceedings of the 27th International Symposium on Temporal Representation and Reasoning, 2020
2019
Automatic white-box testing of first-order logic ontologies.
J. Log. Comput., 2019
A Framework for the Evaluation of SUMO-Based Ontologies Using WordNet.
IEEE Access, 2019
Towards Certified Model Checking for PLTL Using One-Pass Tableaux.
Proceedings of the 26th International Symposium on Temporal Representation and Reasoning, 2019
2018
Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach.
Proceedings of the 25th International Symposium on Temporal Representation and Reasoning, 2018
2017
Black-box Testing of First-Order Logic Ontologies Using WordNet.
CoRR, 2017
2016
A Tutorial on Using Dafny to Construct Verified Software.
Proceedings of the Proceedings XVI Jornadas sobre Programación y Lenguajes, 2016
Evaluating Automated Theorem Provers Using Adimen-SUMO.
Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016
2015
An Assertional Proof of the Stability and Correctness of Natural Mergesort.
ACM Trans. Comput. Log., 2015
Evaluating the Competency of a First-Order Ontology.
Proceedings of the 8th International Conference on Knowledge Capture, 2015
Improving the Competency of First-Order Ontologies.
Proceedings of the 8th International Conference on Knowledge Capture, 2015
2013
Logical foundations for more expressive declarative temporal logic programming languages.
ACM Trans. Comput. Log., 2013
Invariant-Free Clausal Temporal Resolution.
J. Autom. Reason., 2013
2012
Adimen-SUMO: Reengineering an Ontology for First-Order Reasoning.
Int. J. Semantic Web Inf. Syst., 2012
2010
Translating propositional extended conjunctions of Horn clauses into Boolean circuits.
Theor. Comput. Sci., 2010
2009
Dual Systems of Tableaux and Sequents for PLTL.
J. Log. Algebraic Methods Program., 2009
Proceedings of the Ninth Spanish Conference on Programming and Languages, 2009
2008
A Functorial Framework for Constraint Normal Logic Programming.
Appl. Categorical Struct., 2008
A Generalization of the Folding Rule for the Clark-Kunen Semantics.
Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008
2007
Systematic Semantic Tableaux for PLTL.
Proceedings of the Seventh Spanish Conference on Programming and Computer Languages, 2007
A New Proposal Of Quasi-Solved Form For Equality Constraint Solving.
Proceedings of the Seventh Spanish Conference on Programming and Computer Languages, 2007
A Cut-Free and Invariant-Free Sequent Calculus for PLTL.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007
2006
Proceedings of the Sixth Spanish Conference on Programming and Languages, 2006
Equational Constraint Solving Via a Restricted Form of Universal Quantification.
Proceedings of the Foundations of Information and Knowledge Systems, 2006
2005
An Algorithm for Local Variable Elimination in Normal Logic Programs.
Proceedings of the Logic Based Program Synthesis and Transformation, 2005
2004
Elimination of Local Variables from Definite Logic Programs.
Proceedings of the Fourth Spanish Conference on Programming and Computer Languages, 2004
Constructive negation by bottom-up computation of literal answers.
Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), 2004
2000
Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic.
Proceedings of the Frontiers of Combining Systems, 2000
1999
An Algebraic Framework for the Definition of Compositional Semantics of Normal Logic Programs.
J. Log. Program., 1999
A Strong Logic Programming View for Static Embedded Implications.
Proceedings of the Foundations of Software Science and Computation Structure, 1999
1997
A Monotonic Declarative Semantics for Normal Logic Programs.
Proceedings of the 1997 Joint Conf. on Declarative Programming, 1997
1992
Reasoning with Higher Order Partial Functions.
Proceedings of the Computer Science Logic, 6th Workshop, 1992
1990
A First Order Logic for Partial Functions.
Theor. Comput. Sci., 1990
1989
A First Order Logic for Partial Functions (Extended Abstract).
Proceedings of the STACS 89, 1989
1988
Some General Incompleteness Results for Partial Correctness Logics
Inf. Comput., October, 1988