A Resolution Prover for Coalition Logic [PDF]
Electronic Proceedings in Theoretical Computer Science, 2014 We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency.
Cláudia Nalon +3 more
doaj +8 more sources
A Finite-Model-Theoretic View on Propositional Proof Complexity [PDF]
Logical Methods in Computer Science, 2022 We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded-width resolution, and the ...
Erich Grädel +3 more
doaj +1 more source
α-Generalized lock resolution method in linguistic truth-valued lattice-valued logic [PDF]
International Journal of Computational Intelligence Systems, 2012 This paper focuses on effcient non-clausal resolution-based automated reasoning methods and algorithms for a lattice-ordered linguistic truth-valued logic, which corresponds to extensions of α-lock resolution.
Xingxing He +3 more
doaj +1 more source
α-Generalized Semantic Resolution Method in Linguistic Truth-valued Propositional Logic P(X) [PDF]
International Journal of Computational Intelligence Systems, 2014 This paper is focused on α-generalized semantic resolution automated reasoning method in linguistic truth-valued lattice-valued propositional logic.
Jiafeng Zhang, Yang Xu, Xingxing He
doaj +1 more source
α-Quasi-Lock Semantic Resolution Method Based on Lattice-Valued Logic [PDF]
International Journal of Computational Intelligence Systems, 2014 Based on the general form of α-resolution principle for a lattice-valued logic with truth-values defined in a lattice-valued logical algebra structure - lattice implication algebra, the further extended α-resolution method in this lattice ...
Xiaomei Zhong +3 more
doaj +1 more source
α-Minimal Resolution Principle For A Lattice-Valued Logic [PDF]
International Journal of Computational Intelligence Systems, 2015 Based on the academic ideas of resolution-based automated reasoning and the previously established research work on binary α-resolution based automated reasoning schemes in the framework of lattice-valued logic with truth-values in a lattice ...
Hairui Jia, Yang Xu, Yi Liu, Jun Liu
doaj +1 more source
Design of quantum optical experiments with logic artificial intelligence [PDF]
Quantum, 2022 Logic Artificial Intelligence (AI) is a subfield of AI where variables can take two defined arguments, True or False, and are arranged in clauses that follow the rules of formal logic.
Alba Cervera-Lierta +2 more
doaj +1 more source
Structural Resolution for Abstract Compilation of Object-Oriented Languages [PDF]
Electronic Proceedings in Theoretical Computer Science, 2017 We propose abstract compilation for precise static type analysis of object-oriented languages based on coinductive logic programming. Source code is translated to a logic program, then type-checking and inference problems amount to queries to be solved ...
Luca Franceschini +2 more
doaj +1 more source
Determination of 3-Ary -Resolution in Lattice-valued Propositional Logic LP(X) [PDF]
International Journal of Computational Intelligence Systems, 2013 One of key issues for -() ary resolution automated reasoning based on lattice-valued logic with truth-value in a lattice implication algebra is to investigate the -() ary resolution of some generalized literals.
Yi Liu, Hairui Jia, Yang Xu
doaj +1 more source
α-Resolution Method for Lattice-valued Horn Generalized Clauses in Lattice-valued Propositional Logic Systems [PDF]
International Journal of Computational Intelligence Systems, 2015 In this paper, an α-resolution method for a set of lattice-valued Horn generalized clauses is established in lattice-valued propositional logic system ℒ P(X) based on lattice implication algebra.
Weitao Xu +4 more
doaj +1 more source