6 citations · 15 across the 16 of their papers we have counts for
13 papers · 1 filter
Eigenvariables, bracketing and the decidability of positive minimal predicate logic
Gilles Dowek, Ying Jiang
We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of seq…
Enumerating proofs of positive formulae
Gilles Dowek, Ying Jiang
We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of…
On the Expressive Power of Schemes
Gilles Dowek, Ying Jiang
We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike -calculus, the syntax of this calculus sticks clo…
Complementation: a bridge between finite and infinite proofs
Gilles Dowek, Ying Jiang
When a proposition has no proof in an inference system, it is sometimes useful to build a counter-proof explaining, step by step, the reason of this non-provability. In general, th…
VMDV: A 3D Visualization Tool for Modeling, Demonstration, and Verification
Jian Liu, Ying Jiang, Yanyun Chen +1
The output of an automated theorem prover is usually presented by using a text format, they are often too heavy to be understood. In model checking setting, it would be helpful if…
Modeling and Reasoning About Wireless Networks: A Graph-based Calculus Approach
Shichao Liu, Ying Jiang
We propose a graph-based process calculus for modeling and reasoning about wireless networks with local broadcasts. Graphs are used at syntactical level to describe the topological…