Concept
Tautology (logic)
Related publications (12)
LISA – A Modern Proof System
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...
2023On the Power and Limitations of Branch and Cut
The Stabbing Planes proof system [Paul Beame et al., 2018] was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formu ...
Schloss Dagstuhl - Leibniz-Zentrum für Informatik2021Improving Circuit Mapping Performance Through MIG-based Synthesis for Carry Chains
Giovanni De Micheli, Paolo Ienne, Mathias Soeken, Grace Zgheib, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Xifan Tang, Ana Petkovska, Zhufei Chu
Hard-wired carry chains in FPGAs are designed to improve efficiency of important arithmetic primitives. Although they are proven to be effective for arithmetic-rich functions, there are very few studies on the optimization opportunities of carry chains for ...
ACM2017Exploiting Satisfiability Solvers for Efficient Logic Synthesis
Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...
EPFL2017Method for speeding up boolean satisfiability
Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù
A method for transforming a tautology check of an original logic circuit into a contradiction check of the original logic circuit and vice versa comprises interpreting the original logic circuit in terms of AND, OR, MAJ, MIN, XOR, XNOR, INV original logic ...
2016Exploiting Circuit Duality to Speed Up SAT
Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Maciej Jerzy Ciesielski
In this paper, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check dete ...
IEEE2015Towards Complete Reasoning about Axiomatic Specifications
To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011On Complete Reasoning about Axiomatic Specifications
Automated software verification tools typically accept specifications of functions in terms of pre- and postconditions. However, many properties of functional programs can be more naturally specified using a more general form of universally quantified prop ...
2010Evolving Objects in Temporal Information Systems
Stefano Spaccapietra, Christine Parent
This paper presents a semantic foundation of temporal conceptual models used to design temporal information systems. We consider a modelling language able to express both timestamping and evolution constraints. We conduct a deeper investigation of evolutio ...
2007Extending OWL with Explicit Dependency
Functional Dependency has been extensively studied in database theory. It provides an elegant formalism for specifying key constraints and is the basis for normalization theory used in Relational database design. Given its known axiomatization through logi ...
2007