Yun-Rong Luo |  Aman Goel... -  《Leveraging Applications of Formal Methods,Verification and Validation,Part III.Specification and Verification》 -  International Symposium on Leveraging Applications of Formal Methods,Verification and Validation - 2025, - 374～384 - 共11页

摘要：In prior work, we introduced a procedure for |  deriving minimum formulas in first-order logic (FOL) for |  the reachable states of a restricted class of multi | -sorted distributed protocol specifications: protocols |  with sorts representing unbounded sets of symmetric

关键词： Distributed protocols |  Logic minimization |  Invariant inference |  Symmetry |  Quantifier inference |  Reachable states

Eden Frenkel |  Tej Chajed... -  《Computer Aided Verification: 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II》 -  International Conference on Computer Aided Verification - 2024, - 86～108 - 共23页

摘要：This paper lays a practical foundation for |  using abstract interpretation with an abstract domain |  that consists of sets of quantified first-order logic |  formulas. This abstract domain seems infeasible at first |  sight due to the complexity of the formulas involved

关键词： Abstract interpretation |  First-order logic |  Symbolic abstraction |  Invariant inference |  Quantifier alternation |  Least fixpoint

Juha Kontinen |  Max Sandstrom... -  《Foundations of Information and Knowledge Systems: 13th International Symposium, FoIKS 2024, Sheffield, UK, April 8-11, 2024, Proceedings》 -  International Symposium on Foundations of Information and Knowledge Systems - 2024, - 275～286 - 共12页

摘要：-inference in information flow security, cannot be |  restricted to one universal quantifier, while the left |  quantifier. | Linear temporal logic (LTL) is used in system |  verification to write formal specifications for reactive

关键词： Hyperproperties |  Temporal logic |  Team semantics |  HyperLTL |  Verification

Patrick Doherty |  Andrzej Szalas -  《Artificial Intelligence: An International Journal》 - 2024,326(Jan.) - 104036.1～104036.18 - 共18页

摘要： characterized in terms of entailment and inference, rather |  quantifier elimination and the use of Ackermann's Lemma and | Forgetting is an important concept in |  knowledge representation and automated reasoning with |  widespread applications across a number of disciplines. A

关键词： Knowledge representation and reasoning |  Forgetting |  Weakest sufficient conditions |  Strongest necessary conditions |  Quantifier elimination

Safranek, Dominik |  Thingna, Juzar -  《Physical Review, A》 - 2023,108(3 Pt.A) - ARTN 032413～ - 共23页 - 被引量：1

摘要： entropy is a well-defined quantifier determining how |  tool for quantum-state inference. Further developed | Observational entropy is interpreted as the |  uncertainty an observer making measurements associates with |  a system. So far, properties that make such an

关键词： KOLMOGOROV-SINAI ENTROPY |  STATE TOMOGRAPHY |  BOLTZMANN |  EQUILIBRIUM |  FOUNDATIONS |  GIBBS

Koenig, Jason R. |  Padon, Oded... -  《Tools and algorithms for the construction and analysis of systems, part 1: 28th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2022), held as part of the European joint conferences on theory and practice of software (ETAPS 2022), April 2–7, 2022, Munich, Germany》 -  European joint conferences on theory and practice of software - 2022, - 338～356 - 共19页

摘要： inductive invariants with quantifier alternations. We |  for quantifier-free bodies. The breadth-first | -suited to lemmas with quantifier alternations by |  quantifier-free body, while carefully controlling the size | ) well-defined syntactic metrics for simple quantifier

关键词： invariant inference |  quantifier alternation |  PDR/IC3

NSTL主题词： taming |  ALTERNATIONS |  Invariant |  Explosions

Kana Koyano |  Hitomi Yanaka... -  《18th Joint ACL-ISO Workshop on Interoperable Semantic Annotation: 18th Joint ACL-ISO Workshop on Interoperable Semantic Annotation (ISA-18), held at Language Resources and Evaluation Conference (LREC), 20-25 June 2022, Marseille, France》 -  Joint ACL-ISO Workshop on Interoperable Semantic Annotation - 2022, - 127～132 - 共6页

摘要： characterized by the flexibility of quantifier positions and |  construct an inference test set for numerical expressions |  our inference test set poses challenges for |  inference involving various types of numeral expressions. | Numeral expressions in Japanese are

关键词： numeral expressions |  Japanese |  natural language inference |  entailment |  implicature

Backeman, Peter |  Rummer, Philipp... -  《Formal methods in system design》 - 2021,57(2) - 121～156 - 共36页

摘要：The inference of program invariants over |  well as bit-vector quantifier elimination (QE), that |  machine arithmetic, commonly called bit-vector |  arithmetic, is an important problem in verification | . Techniques that have been successful for unbounded

关键词： Bit-vectors |  Interpolation |  Quantifier elimination |  Presburger arithmetic

Tudor Jebelean -  《Intelligent Computer Mathematics: 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings》 -  International Conference on Intelligent Computer Mathematics - 2021, - 130～134 - 共5页

摘要： continuity of functions. Additionally to general inference |  alternating quantifiers, use of Quantifier Elimination by | We present a plug-in to the Theorema system | , which generates proofs similar to those produced by |  humans for theorems in elementary analysis and is based

关键词： Satisfiability checking |  Natural-style proofs |  Computer algebra |  Symbolic computation |  Satisfiability modulo theories

NSTL主题词： ultimate analysis |  Heuristics

Kazutaka Matsuda -  《Programming Languages and Systems: 29th European Symposium on Programming (ESOP 2020), Held as Part of the 23rd European Joint Conferences on Theory and Practice of Software (ETAPS 2020), 25–30 April 2020, Dublin, Ireland》 -  European Joint Conferences on Theory and Practice of Software - 2020, - 456～483 - 共28页

摘要： the type inference of λ_→~q. Although the Linear |  Haskell implementation is equipped with type inference |  inference system for a rank 1 qualified-typed variant of |  this ambiguity issue through quantifier elimination | Bernardy et al. [2018] proposed a linear type

关键词： Linear Types |  Type Inference |  Qualified Typing.

NSTL主题词： linear type |  Modularity |  Linear