scientific article; zbMATH DE number 7552282

DOI10.13137/2464-8728/33309MaRDI QIDQ5087785zbMATH OpenFDO

Authors Maximiliano Cristiá, Gianfranco Rossi

Publication date 1 July 2022

Full work available at URL https://arxiv.org/abs/2104.08130

zbMATH Keywords

formal verificationset theorydeclarative programmingset programming

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other classical set theory (including functions, relations, and set algebra) (03E20) Applications of set theory (03E75) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• {log}: A language for programming in logic with finite sets
• Logic programming and logarithmic space
• From formulas to cirquents in computability logic
• scientific article; zbMATH DE number 1368923
• THE Σλ-CALCULUS AND DERIVED PROGRAM FORMS
• Algebra and Coalgebra in Computer Science
• A program transformation from equational programs into logic programs
• scientific article; zbMATH DE number 3846863
• Logic Programs for Primitive Recursive Sets
• The satisfiability of logical formula in proof of program

Cites work

• scientific article; zbMATH DE number 3976287 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 53088 (Why is no real title available?)
• scientific article; zbMATH DE number 1368923 (Why is no real title available?)
• scientific article; zbMATH DE number 2086594 (Why is no real title available?)
• A complete and terminating approach to linear integer solving
• A decision procedure for restricted intensional sets
• A decision procedure for sets, binary relations and partial functions
• A pearl on SAT and SMT solving in Prolog
• A set solver for finite set relation algebra
• Abstract state machines, Alloy, B, TLA, VDM, and Z. 6th international conference, ABZ 2018, Southampton, UK, June 5--8, 2018. Proceedings
• An automatically verified prototype of the Tokeneer ID station specification
• Automated proof of Bell-LaPadula security properties
• Automated reasoning with restricted intensional sets
• Cardinality constraints for arrays (decidability results and applications)
• Efficient automated reasoning about sets and multisets with cardinality constraints
• Proofs as programs
• Set unification
• Solving quantifier-free first-order constraints over finite sets and binary relations
• The calculus of constructions
• {log}: A language for programming in logic with finite sets

Cited in

(6)

• A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
• MUNCH -- automated reasoner for sets and multisets
• A set solver for finite set relation algebra
• CLAIRE: combining sets, search and rules to better express algorithms
• LOIS: syntax and semantics
• scientific article; zbMATH DE number 5072506 (Why is no real title available?)

Describes a project that uses

Uses Software

• Z
• SETL

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5087785)